ChatGPT provides mathematical proof autonomously

ChatGPT has succeeded in providing proof that verifies a conjecture from 2024 put forward by the mathematicians Ran and Teng. A conjecture is a statement that is believed to be true because there are many examples or indications supporting it, but for which no formal proof yet exists. Mathematicians often formulate such a conjecture after discovering a pattern or following numerous calculations that consistently yield the same result. Until someone provides conclusive proof, it remains a conjecture; once it is proven, it becomes a proposition or theorem.

The study describes how seven chat sessions with ChatGPT and four versions of the proof collectively produced the final proof. ChatGPT proved particularly useful in the search for the proof, whilst human experts were essential for verifying its accuracy and ensuring the argument was watertight.

The authors demonstrate that ChatGPT-5.2 (Thinking) largely developed the structure of the proof itself, with minimal human intervention. As the paper’s brief description summarises: “With the Data Analytics Lab, we are among the first to demonstrate that a commercially available LLM can independently develop original mathematical proofs.”

“I had long suspected that ChatGPT could help me with the proof of unsolved mathematical problems,” says Brecht Verbeken, a postdoctoral researcher in the Data Analytics Lab research group at the VUB. “And yet I was surprised at how efficiently it went.”

The researchers situate their work within the broader context of what they call ‘vibe-proving’, an approach in which language models are used to explore and structure high-level theoretical reasoning. The key question in the publication is whether this vibe-proving technique will undergo the same rapid evolution over the coming year as previously seen with AI-assisted programming (vibe-coding), where systems developed from tools into virtually autonomous code generators. “We often hear people say that the creativity of these systems is fundamentally limited to reformulating training data,” says VUB professor Vincent Ginis (Data Analytics Lab). “I’m glad we can dispel that misconception with our work too…”

The authors emphasise that, although the model generated a substantial part of the proof scheme itself, humans remain crucial for the final check and for closing formal gaps. Above all, the process clearly demonstrates where LLM assistance really makes a difference and where verification bottlenecks remain. This development marks an important moment in the use of AI within theoretical research: not only as an aid to programming and text production, but as a tool that can contribute to original mathematical discoveries. Although this must still be coupled with human supervision and critical reasoning. “Formulating candidate proofs can now be done much faster, but the bottleneck then becomes human verification. That takes time. But the language models will surely help us there too,” concludes VUB Professor Andres Algaba (Data Analytics Lab VUB).