IMPLICATOR
The working group behind the Leiden Declaration on Artificial Intelligence and Mathematics published an 11-page statement Tuesday saying mathematicians should disclose AI tools, retain responsibility for correctness and keep automated systems out of authorship. The International Mathematical Union has endorsed the statement, which was written by 16 researchers after a September 2025 workshop in Leiden.
The timing comes from OpenAI’s May 20 announcement. OpenAI said an internal model had disproved the planar unit distance conjecture, an 80-year-old Erdős problem in discrete geometry. The proof now has a human-digested companion paper, but the model itself is not public.
The declaration’s practical claim is that AI proof has become a review problem, not only a capability story. If a private model can produce publishable mathematics, journals need a record of the tools, compute and human work behind it before referees can judge the result.
Key Takeaways
- Sixteen researchers published the Leiden Declaration after OpenAI’s Erdős proof.
- The IMU endorsement puts AI proof disclosure in front of global mathematics.
- The declaration asks authors to list AI tools and compute resources.
- The proof was praised, but its proprietary model remains the transparency problem.
AI-generated summary, reviewed by an editor. More on our AI guidelines.
Tool disclosure in papers
The declaration’s first recommendation for individual mathematicians tells authors to add a “Tool and computational resource disclosure” section to papers. The list names large language models, machine-learning systems, proof assistants, mathematical software and, where relevant, the resources used to run them.
A journal rule based on that language would give referees model and compute information before review. The same section says human authors remain responsible for correctness, citations and any significant recommendation they make as reviewers.
Leiden University said the statement came from 16 researchers at 15 universities after a September 2025 workshop that drew around 60 participants from 10 countries. Rodrigo Ochigame, the Leiden anthropologist of AI who helped write it, said the group spent months “bringing together different points of view in search of shared principles.”
Martin, the Oxford mathematician and computer scientist, told The New York Times the document is “a provocation, a stimulus for debate.” Ulrike Tillmann, the IMU’s vice president, wrote in the Leiden University release that mathematical research should be guided by “human judgment, fair and transparent practices, and the shared values of the global mathematical community.”
What OpenAI’s proof changed
Erdős problem 90, posed in 1946, asks for the maximum number of unit-distance pairs determined by n points in the Euclidean plane. Erdős had conjectured an upper bound of n^(1+o(1)); the best current upper bound, the arXiv companion paper notes, remains O(n^(4/3)) from Spencer, Szemerédi and Trotter in 1984.
OpenAI said its internal model produced an infinite family of point sets with at least n^(1+epsilon) unit-distance pairs, disproving the long-held upper-bound conjecture. The companion paper states that the original proof was generated “in one shot” by an internal model, then refined through human interactions with Codex and rewritten into a human-digested proof.
Several prominent mathematicians responded in direct terms. Tim Gowers called the result “a milestone in AI mathematics.” Jacob Tsimerman of the University of Toronto told the Times, “This is a really impressive piece of work, and I would accept it for any journal without hesitation.” Arul Shankar wrote that current models can have “original ingenious ideas” and carry them through.
Get the signal behind AI’s next research shift
Strategic AI news from San Francisco. No hype, no "AI will change everything" throat clearing. Just what moved, who won, and why it matters. Daily at 6am PST.
No spam. Unsubscribe anytime.
What OpenAI did not disclose
OpenAI’s blog post framed the proof as evidence that better mathematical reasoning could make AI a “stronger research partner” in science and engineering. The company also said the model was general-purpose, not a system trained specifically for the unit distance problem.
The Leiden document points to the missing record. It warns that public claims about AI proofs can outrun scientific review when they arrive through press releases or blog posts without the information needed to evaluate them. Ochigame gave the sharper version to the Times: no outside access to the model, no public account of the detailed methods, training data or compute.
“The A.I. model is proprietary and unavailable to anyone outside the company,” Ochigame said. “We get a flashy promotional video, while basic information needed to assess the scientific meaning of the result is kept secret.”
Matchett Wood gave a narrower mathematical concern. She called AI “a powerful tool” that could speed research, but said mathematicians need to use it “in a way that will maintain human understanding of the mathematics.” She also said the OpenAI paper did not properly reference a history of closely related ideas.
Know someone who'd find this useful? ✉️ Email it to a friend in one click, or they can subscribe free here.
The companion paper makes the proof credible; it does not settle the governance questions. The remaining questions are attribution, access and whether researchers outside OpenAI can reproduce the work without the same private system.
The nine-author companion paper
The arXiv abstract calls the paper a “human-verified” version of OpenAI’s counterexample. Its nine authors present a “human-digested, somewhat simplified, and somewhat generalized version” of the AI proof, then add reflections on how the construction fits the field.
Thomas Bloom wrote that the original AI proof was “completely valid,” but “significantly improved” by OpenAI researchers and the mathematicians involved in the paper. He also pointed to the human work of “discussing, digesting, and improving this proof, and exploring its consequences.”
Will Sawin found a refinement with an explicit exponent delta = 0.014, according to OpenAI’s post, while the companion paper describes the initial proof’s exponent only as some positive value. The proof became more useful after mathematicians worked on it.
Private systems were already the concern in The Implicator’s earlier coverage of AI mathematics. OpenAI, Google DeepMind and Harmonic controlled many of the high-value tools named in that article; the Leiden document now puts disclosure language next to the same access problem.
The declaration’s ICM session is scheduled for July 23-30 in Philadelphia. By then, journals and mathematical societies will have the IMU-endorsed text in hand and a recent OpenAI proof to measure it against.
Frequently Asked Questions
What is the Leiden Declaration?
It is a June 2026 statement from 16 researchers setting proposed norms for AI use in mathematics, including disclosure, human responsibility, attribution and institutional policy.
Why did OpenAI’s Erdős proof matter?
OpenAI said an internal model disproved the 80-year-old planar unit distance conjecture, one of Paul Erdős’s well-known discrete geometry problems.
Does the declaration try to ban AI from mathematics?
No. It treats AI as a tool, but argues that mathematicians, journals and funders need clear rules for attribution, verification and access.
What is the main transparency concern?
The OpenAI proof came from a proprietary internal model. Critics say outsiders cannot inspect the model, detailed methods, training data or compute used.
What happens next?
The declaration is scheduled for discussion at the International Congress of Mathematicians in Philadelphia from July 23 to July 30.
AI-generated summary, reviewed by an editor. More on our AI guidelines.
Marcus Schuler
Editor-in-Chief and founder of Implicator.ai. Former ARD correspondent and senior broadcast journalist with 10+ years covering tech. Writes daily briefings on policy and market developments. Based in San Francisco. E-mail: editor@implicator.ai
