When AI "solves" a conjecture without proof: mathematicians push back

Imagine an AI model announcing that it has solved an eighty-year-old geometric conjecture. No proof published in a peer-reviewed journal, no source code available, no training data disclosed. Just a press release. To a mathematician, that is about as convincing as a magician claiming to have discovered the law of gravity because he can make a hat levitate.

It is precisely this kind of situation — reported by Ars Technica two weeks after an OpenAI announcement of a supposed mathematical result — that prompted the drafting of a collective text that became, within a few weeks, an event in the international mathematics community. The Leiden Declaration on Artificial Intelligence and Mathematics, filed on June 2, 2026 with DOI 10.5281/zenodo.20302944, is not a regulation, not a law, not an anti-technology manifesto. It is something rarer: a set of norms, written by researchers for researchers, at the precise moment when a discipline realizes that its rules of the game are changing without being consulted.

It all begins in September 2025, at a workshop at the Lorentz Center in Leiden titled "Mechanization and Mathematical Research." About sixty participants from ten countries — mathematicians, computer scientists, historians and anthropologists of science — come together to discuss what automation is doing to their discipline. Out of these exchanges comes a working group convened by Jim Portegies, of Eindhoven University of Technology, which spends the following six months building a shared text, as Leiden University recounts.

The result is signed by sixteen authors whose affiliations span Washington, Edinburgh, Amsterdam, Warwick, San Diego, Columbia, Cambridge, Oxford and Zurich. Rodrigo Ochigame, historian and anthropologist of AI at Leiden University and co-author, sums up the ambition: "We worked on the declaration for several months, bringing together different points of view in search of shared principles." The text has since received the endorsement of the International Mathematical Union — the international organization associated notably with the Fields Medals and the International Congress of Mathematicians (ICM). Its secretary general, Christoph Sorger, was keen to clarify: "The IMU endorses the Leiden Declaration because it is a timely, serious and balanced contribution to a debate that is only just beginning." And he added: "This endorsement does not mean the end of the debate."

The text identifies five fundamental values of mathematical research that the current use of AI threatens: the certainty of proofs, the verifiable attribution of results, the transparency of arguments, collective standards of evaluation, and the discipline's autonomy from outside commercial interests.

The first threat is perhaps the most technical — and the most insidious. "Current automated techniques can produce plausible but unreliable, even incorrect, arguments that are difficult to distinguish from genuine mathematical proofs," the declaration warns. You see the problem: a mathematical proof is not a text that resembles a proof. It is a logical object in which every step must be verifiable. A large language model can string symbols together with impressive fluency while making a reasoning error on line 47 — an error that only an attentive human expert will catch.

The distinction is fundamental. As Jeremy Avigad, professor at Carnegie Mellon University, puts it in his article on the formal turn in mathematics: "We can now write definitions, theorems, and proofs in idealized languages, akin to programming languages, that computers can interpret and check." But checking is not generating. And this is exactly where generative AI models are a problem: they generate without guaranteeing.

The second threat concerns attribution and copyright. Mathematicians see their papers, published on arXiv — freely accessible, in the discipline's tradition of openness — scraped to train commercial models, without consent and without compensation. Ochigame puts it bluntly: "Mathematicians who never intended to contribute to the development of AI find their work used for that purpose without their consent."

The third threat, more diffuse, is that of hype — media buzz. Michael Harris, mathematician at Columbia University and co-author of the declaration, delivers the diagnosis with surgical precision: "The tech industry operates according to a commercial logic that is antithetical to the values of mathematics." When a company announces a mathematical result through a press release before any verifiable publication, it short-circuits the process of collective validation that has, for centuries, been at the heart of mathematical practice.

Behind the ethical stakes lies a precise mathematical and computational question. How can we know that a proof is correct if we cannot check it ourselves? The community of formal proof assistants — software such as Lean or Coq — has, since the 1970s, developed an elegant answer: the de Bruijn criterion. As Henk Barendregt and Freek Wiedijk explain in their foundational article on the challenge of computational mathematics, a proof assistant satisfies this criterion if the proof it produces can be independently checked by a small verification program, separate from the system that helped build it. Trust rests not on the intelligence of the generator, but on the transparency of the verifier.

This is exactly what proprietary AI models do not provide. When the model is inaccessible, as Ochigame points out, "the AI model is proprietary and unavailable to anyone outside the company" — no de Bruijn criterion is possible. No independent verification. No proof in the mathematical sense of the word.

The Mathlib library, developed for the Lean proof assistant and described in the mathlib community's article, illustrates the alternative: a community-built corpus of verified definitions, theorems and proofs, covering algebra, topology, category theory and analysis — built in a distributed way, with no central authority, and freely accessible. This is the model the declaration implicitly champions: open, verifiable, attributable.

The recommendations are precise and actionable. Researchers are asked to explicitly disclose the use of automated tools — large language models, proof assistants, mathematical software — in a dedicated section of their papers. Responsibility for the accuracy of results still rests with humans. Results must not be presented as produced solely by a company or a model when human contributions and prior work are involved. And authors must be able to refuse to let their publications be used as training data.

The declaration does not call for banning AI in mathematics. Leslie Ann Goldberg, head of computer science at the University of Oxford and co-signatory, states the real risk soberly: "Inaccurate AI-generated drafts are cheap to produce, and there is a risk of cluttering the literature with claimed results that are simply wrong." The problem is not the tool. It is the absence of norms for using it.

Peter Scholze, director of the Max Planck Institute for Mathematics and a Fields Medalist, sums up the philosophical stakes: "The purpose of mathematical research is human understanding of mathematics, so mathematics can only thrive in a community of human researchers." The declaration itself puts it in one sentence: "Mathematics is, and must always remain, a profoundly human endeavor."

A dedicated discussion is planned for July 26, 2026 at ICM 2026, as announced by IMU News in May 2026. The debate is only just beginning.

To understand precisely what is at stake, we need to distinguish three levels of relationship between AI and mathematical proof.

The first level is mathematical text generation: a large language model produces a text that resembles a proof, in natural language. This is what models such as GPT-4 or Claude do. The problem is that textual plausibility and logical validity are two different things. A model can hallucinate a reasoning step with the same fluency it uses to state a correct lemma.

The second level is formal verification: a proof is written in a formal language — Lean, Coq, Isabelle — that the proof assistant can check mechanically. As Jeremy Avigad and John Harrison showed in their article published in Communications of the ACM, formal verification could become a new standard of rigor in mathematics. Here, trust rests not on the reader's expertise but on the logic of the verifier.

The third level, the most ambitious, is autoformalization: automatically translating a natural-language proof into a verifiable formal object. The ProofNet benchmark, presented in an article by Azerbayev, Piotrowski, Schoelkopf, Ayers, Radev and Avigad, contains 371 examples, each pairing a formal statement in Lean 3, a natural-language statement and a natural-language proof, drawn from undergraduate-level textbooks in real analysis, linear algebra and topology. The result: in their experiments, the Code-davinci-002 model correctly formalized 13.4% of theorems in few-shot mode (that is, with a few examples provided in context) and 16.1% with retrieval of similar prompts. The syntactic verification rate (typecheck rate) reached 45.2% with prompt retrieval — meaning that more than half of the outputs produced did not even pass Lean's syntax check, before any question of mathematical validity.

These figures are not an indictment of AI in mathematics. They simply show that the path from "convincing mathematical text" to "formally verified proof" is still a long one — and that the Leiden Declaration is right to carefully distinguish between the two.