Using AI to Tackle Conway's Conjecture: Vibe Coding Enters the World of Mathematical Proof

When "Vibe Coding" Meets a Mathematical Conjecture

Dan Abramov (gaearon), the well-known frontend engineer and React core contributor, recently published a striking project on GitHub: using AI in a "vibe coding" style, he attempted to construct a proof or refinement of Conway's conjecture. The project garnered 245 upvotes and over 229 comments on Hacker News, sparking intense debate about AI's role in serious mathematical research.

"Vibe coding" is a workflow that has become popular in the developer community: instead of writing code line by line, developers engage in continuous dialogue with large language models, iterating through feedback and letting the AI handle most of the generation work, while humans focus on direction and verification. Abramov's move to apply this methodology to mathematical proof construction — rather than software development — is itself a remarkably experimental undertaking.

What the Project Is Doing

According to the repository's description, Abramov is not claiming to have independently completed a rigorous mathematical proof. Rather, he is documenting the process of collaborating with AI to progressively converge on an argument. The repository includes a dedicated section titled "Why I think it's correct," which honestly lists his reasons for believing the argument holds — rather than announcing a definitive conclusion with any air of authority.

This framing is itself worth noting. It reflects a cautious posture: the "correctness" of a mathematical argument produced with AI assistance requires independent verification, and the author uses "I think" rather than "I proved" to characterize it, leaving judgment to readers and the mathematics community.

Conway's conjecture was proposed by mathematician John Horton Conway and belongs to the domain of open problems in combinatorics or number theory (the specific problem requires confirmation from the repository context — Conway proposed numerous famous conjectures throughout his life, including propositions related to integer sequences and game theory). What Conway's conjectures share is that their statements tend to be concise and intuitive, yet rigorous proofs are extremely difficult and require deep structural insight. For this reason, it makes an interesting target for testing AI's mathematical capabilities — specific enough to be well-documented, yet far from "trivialized." Abramov's choice of this problem over a textbook exercise signals that his goal is to probe the boundaries of AI on genuine open problems, not to demonstrate AI completing tasks that are already known to be solvable.

A Polarized Community Response

The discussion on Hacker News showed a clear divide.

One camp was optimistic and curious, arguing that experiments like this demonstrate AI's potential as a "cognitive amplifier." For exploratory mathematical work, AI's ability to rapidly generate candidate ideas, fill in derivation details, and check symbolic computations can genuinely improve efficiency. Even if the final proof still requires human rigorization, AI plays a valuable role as a "drafting partner."

The other camp remained cautious. They pointed out that mathematical arguments generated by large language models are highly prone to appearing correct while actually being wrong — a logical leap, hidden assumption, or notational abuse buried in a derivation often requires a professional mathematician to examine it word by word before it can be caught. The value of a mathematical proof lies precisely in its rigor, and the intuitive, "vibes"-based judgment style is in inherent tension with that rigor. Evaluating a proof with "I feel like it's right" was exactly what many commenters found troubling.

The Real Limits of AI-Assisted Mathematics

This project touches on a larger question: to what extent can AI genuinely participate in mathematical proof?

Currently, the combination of formal proof assistants (such as Lean and Coq) with AI is considered the more reliable direction — AI generates proof strategies while the formal system mechanically verifies the correctness of each step, eliminating the illusion of "looks right." In contrast, pure natural-language AI arguments lack this layer of mechanical verification, and correctness depends entirely on human oversight.

Abramov's experiment falls into the latter category. It resembles a publicly shared exploration log more than a directly citable result. Its value lies not in whether Conway's conjecture has actually been proved, but in laying out the process, methodology, and limitations of AI-assisted mathematics for the community to discuss.

Formal proof assistants are software systems that translate mathematical language into computer-verifiable logic. Lean and Coq are the most representative examples: users write theorems and proofs step by step in a specialized formal language, and the system mechanically checks every inferential step — any logical gap causes a compilation failure. This is fundamentally different from natural-language proofs, which rely on readers' mathematical intuition to "fill in" steps the author omits, whereas formal systems permit no implicit jumps. In recent years, projects such as DeepMind's AlphaProof and Meta's COPRA have been exploring the use of large language models to automatically generate Lean proof scripts, which Lean then verifies — combining AI's generative capacity with the rigor of formal systems. This approach is widely considered more trustworthy than pure natural-language argumentation, because the illusion of "looks right" cannot pass a formal system's verification.

An Experiment Worth Watching

For developers and AI observers, this project offers a concrete case study for thinking about whether AI collaboration methodologies can cross domain boundaries. In software development, compilers and tests serve as immediate feedback mechanisms; in mathematical proof, no equivalent automatic verification exists, which dramatically raises the weight of human judgment.

As a prominent figure in the technical community, Abramov shared this attempt openly and honestly — including his uncertainties. Regardless of whether the argument ultimately withstands scrutiny from mathematicians, the stance of "making both the process and the doubts public" itself offers an interesting reference point for knowledge production in the age of AI.

Conclusion

AI is permeating more and more domains that require rigorous reasoning. Mathematical challenges like Conway's conjecture may not yet be objects that large language models can independently conquer, but the boundaries of human-AI collaborative exploration are being probed continuously. The real question is not "can AI prove it" but "how do we verify the arguments AI produces" — and that checkpoint remains firmly in human hands.