⏱️ Lectura: 10 min
Twenty-five Fields Medalists, including Terence Tao and Peter Scholze, signed a public declaration warning about the growing use of AI in mathematics. The text, published on mathandai.org under the title “Math and AI,” speaks of a “severe misalignment” between the goals of artificial intelligence companies and those of the mathematical community.
📑 En este artículo
The letter comes after months in which language models improved their ability to solve complex mathematical problems, including several considered to have no known solution. The signatories are not asking for AI to be banned: they are asking the community, companies, and society to urgently confront how this technology is changing the craft of doing mathematics.
TL;DR
- Twenty-five Fields Medalists signed the “Math and AI” declaration, published on mathandai.org.
- Signatories include Terence Tao, Peter Scholze, Maryna Viazovska, and Pierre Deligne.
- The text denounces a “severe misalignment” between AI companies and the mathematical community.
- The signatories say AI already solves major problems with no known solution across several fields.
- The letter calls for time for writeups, attribution, and the integration of AI-generated results.
- The site lets anyone add a public signature via the “Endorse the Declaration” button.
- The authors compare the risk to that faced by other creative and scientific professions confronting AI.
Introduction
AI in mathematics is no longer a laboratory curiosity. In recent months, various language models have started solving problems that had been open for decades in areas like number theory, combinatorics, and algebraic geometry. That leap in capability is precisely what worries the 25 Fields Medalists who signed the “Math and AI” declaration.
The signatories are no strangers to the field: they are people who defined much of the mathematics of the last four decades. Their concern isn’t whether AI “thinks” or “doesn’t think.” It’s that the goal of the companies developing these systems (hitting a milestone, winning a benchmark, making headlines) clashes with the goal of the mathematical community, which is building shared understanding over the long term.
What Happened
The text was published on mathandai.org under the title “Declaration, Math and AI” and carries the signatures of 25 Fields Medalists, including Terence Tao (2006), Peter Scholze (2018), Maryna Viazovska (2022), Pierre Deligne (1978), and Yu Deng (2026). The list spans almost five decades of laureates, from 1978 to the 2026 edition.
The declaration argues that the “dramatic” improvement in the mathematical abilities of language models now lets them “solve major problems with no known solution across many fields of mathematics.” But it warns that this achievement, when pursued as a benchmark, is “harmful to mathematical science and to the mathematical community.”
The document describes three concrete problems. First, haste: many results are announced without a proper writeup, without isolating the new method, and without citing the prior work of other mathematicians. Second, attribution: without that process, open questions of plagiarism and authorship remain. Third, transmission: without mathematicians willing to integrate and develop an AI-generated idea, that idea “never becomes fully alive” within the mathematical canon.
The site includes an “Endorse the Declaration” button so anyone can add their public signature, extending the reach beyond the original 25 medalists.
Context and History
To understand the alarm, you have to understand how mathematical research works. For generations, famous problems served as beacons: solving one was proof that a new idea, an interesting method, existed. That result then went through years of talks, discussions, and simplifications until it reached a textbook that any undergraduate could understand.
The declaration describes the mathematical community as “a miniature version of humanity”: people with different approaches, united by core values. The most valuable resource isn’t papers, it’s students and ideas, and both are cultivated through processes that require time and direct human interaction.
That process clashes with the product logic of an AI company. A model that solves an open problem in a weekend hasn’t gone through the discussion filter that, according to the signatories, is what actually turns a solution into transmissible mathematical knowledge. Publishing the result without that filter doesn’t accelerate mathematics: according to the letter, it can “destroy fertile ground” instead of giving life to new ideas.
📌 Note: the declaration doesn’t question the correctness of the solutions AI produces. It questions what happens afterward: who reviews, who attributes, and who passes that knowledge on to the next generation.
Technical Details: The Advance of AI in Mathematics
The declaration doesn’t give benchmark figures or ask for them to be measured: that’s exactly its point. The way of “measuring” the advance of AI in mathematics that the signatories criticize is counting how many problems a model solves, without verifying whether that solution brings new understanding. Facing that gap, the mathematical community already has a tool that does allow a result to be verified without depending on the reputation of whoever produced it: formal proof assistants, like Lean 4.
A formal proof assistant forces every step of a proof to be written in a language that a computer can check line by line. It doesn’t matter whether the draft came from a human mathematician or a language model: if the file compiles, the proof is valid. This is the kind of independent verification the declaration calls for to separate “solving a problem” from “producing reliable mathematical knowledge.”
Installing Lean 4 takes a few minutes with elan, the official toolchain installer:
# Windows (PowerShell)
irm https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | iex
# macOS
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Linux
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | shWith the toolchain installed, you can formalize and verify a basic proof, like the irrationality of the square root of 2, in a file called Irracional.lean:
import Mathlib.Data.Real.Irrational
theorem raiz_de_dos_irracional : Irrational (Real.sqrt 2) := by
exact irrational_sqrt_two
#check raiz_de_dos_irracionalRunning lake build, Lean compiles the file and confirms the theorem is valid within its type system. If someone replaces the proof with an argument generated by a language model, the check is exactly the same: Lean doesn’t ask the author who they are, only whether the proof closes.
| Verification Method | When to Use It | Advantage | Limitation |
|---|---|---|---|
| Traditional peer review | Results with broad conceptual impact | Evaluates understanding, not just correctness | Slow: can take years in journals |
| Formalization in Lean, Coq, or Isabelle | Proofs with many cases or mechanical steps | Objective verification, independent of the author | Doesn’t evaluate whether the idea is interesting or new |
| Direct announcement without review | Low-priority preprints or work in progress | Fast, immediately visible | No control over attribution or subtle errors |
💭 Key point: the declaration doesn’t say AI in mathematics is useless. It says solving a problem and producing transmissible mathematical knowledge are two different things, and that AI only automates the first.
How to Start Following the Debate
Anyone can read the full text and the list of signatories at mathandai.org. The site adds names in real time through the “Endorse the Declaration” button, so the launch list of 25 Fields Medalists is bound to grow.
For a developer or student who wants to understand firsthand why formalization matters so much in this debate, the shortest path is to install Lean with the commands above and try formalizing a theorem of their own, however simple. The official Lean documentation has an interactive tutorial that runs in the browser, with nothing to install.
You can confirm the environment was installed correctly by running lean --version in the terminal: if it returns a version number instead of a command-not-found error, the toolchain is ready to compile .lean files.
Impact and Analysis
The underlying argument of the declaration goes beyond mathematics. The signatories say so explicitly: they see this as part of “broader alignment problems affecting other scientific and creative professions, as well as society as a whole.” It’s the same pattern already being discussed in programming, design, and writing: AI doesn’t just automate repetitive tasks, it starts directly producing the final output of a training process that used to take years.
In mathematics, that training process serves a double purpose. A student who works through practice problems doesn’t just produce an answer: they develop the ability to formulate new questions. If an AI system hands over the answer directly, that second goal goes unmet, even though the first is achieved faster than ever.
flowchart TD
A["AI system generates a proof"] --> B["Mathematician reviews the result"]
B --> C{"Can it be formalized in Lean?"}
C -->|"Yes"| D["Automatic formal verification"]
C -->|"No"| E["Traditional peer review"]
D --> F["Result accepted by the community"]
E --> F⚠️ Heads up: the declaration warns that announcing results without review opens “serious questions of attribution and plagiarism,” the same risk already faced by other creative professions confronting generative AI.
For mathematicians themselves, the immediate risk is one of incentives. If journals and hiring committees start valuing “how many problems were solved” over “how much new understanding was generated,” the profession ends up optimizing for what AI measures, not for what science needs. The signatories explicitly ask that this decision stay in human hands, not in a benchmark metric.
What’s Next
The declaration doesn’t demand any specific regulatory measure or ask AI companies to stop training models for mathematics. It asks for three things: that the mathematical community openly discuss how to integrate these systems, that companies allow time and give credit before announcing a result, and that society at large treat this as an early case of a bigger challenge.
The site keeps adding signatures after the launch, so the list of supporters is expected to grow in the coming weeks. There is still no formal public response from major AI companies to the points raised in the text. The future of AI in mathematics, the signatories say, will depend on human decisions, not just technical ones.
📖 Summary on Telegram: View summary
Try it yourself: go to mathandai.org, read the full text, and try installing Lean with the commands above to see firsthand how a proof is verified without depending on who wrote it.
Frequently Asked Questions
What is the “Math and AI” declaration?
It’s a public document signed by 25 Fields Medalists warning about a “severe misalignment” between the goals of AI companies and those of the mathematical community, published on mathandai.org.
Who signed the declaration?
The 25 signatories include Terence Tao, Peter Scholze, Maryna Viazovska, Pierre Deligne, Manjul Bhargava, and Cédric Villani, with medals ranging from 1978 to 2026.
Does the declaration call for banning AI in mathematics?
No. It calls for the community, companies, and society to discuss how to integrate these systems without losing the human process of review, attribution, and transmission that sustains the discipline.
What does “severe misalignment” mean in this context?
It refers to the fact that the goal of AI companies (solving problems as a benchmark) clashes with the goal of the mathematical community (generating shared understanding over the long term).
How is an AI-generated proof verified?
By formalizing it in a proof assistant like Lean 4, Coq, or Isabelle: if the file compiles, the proof is valid no matter who wrote it.
Can I add my signature to the declaration?
Yes, the mathandai.org site has an “Endorse the Declaration” button open to anyone who wants to publicly join.
References
- mathandai.org: full text of the “Math and AI” declaration and list of signatories.
- Lean Prover: official documentation for the Lean 4 formal proof assistant.
- Wikipedia: history and full list of Fields Medalists.
- arXiv: preprint repository where the mathematics and AI papers cited in the debate are published.
📱 Do you like this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day.
0 Comments