Chatgpt can autonomously provide mathematical proofs
VUB Data Analytics Lab solves mathematicians Ran and Teng's 2024 conjecture with commercial language model
VUB's Data Analytics Lab publishes new results showing that it is possible to develop original mathematical proofs using commercial language models. In the publication Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterisation with ChatGPT-5.2 (Thinking), the researchers show that OpenAI' s commercial large language model ChatGPT-5.2 (Thinking) could independently solve a mathematical problem.
This particular case involved a proof explaining a 2024 conjecture by mathematicians Ran and Teng. A conjecture is an assertion that is believed to be true because there are many examples or indications of it, but for which no formal proof yet exists. Mathematicians often formulate such a conjecture after discovering a pattern or after many calculations that always give the same result. As long as nobody provides a conclusive proof, it remains a conjecture; as soon as it is proven, it turns into a theorem (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, while human experts were essential for correctness checking and conclusive argumentation.
The authors show that ChatGPT-5.2 (Thinking) largely developed the structure of the evidence itself, with minimal human intervention. As the short description summarises, "With the Data Analytics Lab, we are one of the first to demonstrate that a commercially available LLM can independently develop original mathematical proofs."
"I had long suspected that ChatGPT could help me prove unsolved mathematical problems," says Brecht Verbeken (Postdoctoral researcher in the Data Analytics Lab VUB research group). "And yet I was surprised at how efficiently that worked out."
The researchers place their work in 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 that vibe-proving technique will undergo the same rapid evolution in the coming year as previously seen in AI-assisted programming (vibe-coding), where systems evolved from tools to virtually autonomous code generators. "We often hear how people think that the creativity of systems is fundamentally limited to reformulations of their training data," says VUB professor Vincent Ginis (Data Analytics Lab). "Glad we can dispel that misconception with our work as well."
The authors emphasise that although the model generated a substantial part of the evidence base itself, people are still crucial for the closing verification and closing formal gaps, and that the process offers important insight into where LLM assistance really makes a difference and where verification bottlenecks remain.
The development marks an important moment in the deployment 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, if coupled with human supervision and critical reasoning. "Formulating candidate proofs can now be much faster, but the bottleneck then becomes human verification. That takes time. But language models will help us there too," concludes VUB professor Andres Algaba (Data Analytics Lab VUB).
More info:
Andres Algaba: andres.algaba@vub.be
The publication is freely available via arXiv under identifier 2602.18918 and offers a detailed description of method, results and implications of this early case study in vibe-proving.
Frans Steenhoudt
