Can AI do mathematics? Inside the DESCARTES project with Amaury Hayat
Artificial intelligence has already transformed how we see and understand the world, from decoding protein structures to generating new materials and optimizing energy systems. In 2024, the Nobel Prize in Chemistry went to AI scientists, confirming that machine learning is now part of the scientific canon.
Amaury Hayat (ENPC – Institut Polytechnique de Paris), a Hi! PARIS fellow in the 2025 cohort, sees a new horizon where machines don’t just process data but reason through it. With the DESCARTES project, he investigates how AI might one day assist mathematicians in the art of discovery and proof.
“Our goal,” he explains, “is to see how AI can assist in the very process of mathematical thinking.”
Can a machine discover a theorem?
The team explores two main directions. The first is mathematical discovery, training neural networks to detect promising patterns, generate conjectures, or suggest potential solutions that might inspire human mathematicians. The second is AI theorem proving, designing systems capable of producing verifiable mathematical proofs, combining computational power with human intuition.
Together, these two ambitions outline a new discipline: machine-assisted mathematics.
How AI “reads” mathematical expressions, by encoding equations as trees, a structure used in the DESCARTES project to represent reasoning steps.
A personal equation
Hayat’s motivation is both scientific and deeply personal. “I’m a mathematician first,” he says, “and I’ve always wanted to push research as far as I can, to prove new theorems and build new theories.”
When DeepMind’s AlphaGo defeated world champion Lee Sedol, Hayat was still a student. “One of my first thoughts,” he recalls, “was that if we can train an AI to play Go, then perhaps we can train it to ‘play’ mathematics.”
That idea became a lifelong pursuit. During his PhD, conversations with friends studying AI, among them Alexis Conneau at Meta and Guillaume Lample, also an École Polytechnique alumnus, sparked a collaboration that grew into an international effort. Joined by François Charton, Timothée Lacroix, and others, the group began exploring how neural networks could learn to reason symbolically. “That was the beginning of this fascinating adventure,” Hayat says.
The challenge of teaching machines to reason
Unlike language or images, mathematics doesn’t offer vast troves of data. “The main challenge,” Hayat notes, “is data scarcity.”
In theorem proving, researchers have made progress by curating existing proofs and creating specialized datasets, but at the research frontier, examples are rare by definition. “AI models must learn to operate in a low-data regime, where reinforcement learning becomes crucial,” he explains. “That’s the type of AI that learned to play chess or Go, but ‘playing’ math is far harder.”
Why? Because the number of possible moves in a mathematical proof is astronomically large, and there is no clear feedback until the entire proof is completed. Unlike a game, there’s no opponent to play against, only logic itself.
Another layer of complexity arises from trust. Advanced reasoning models like GPT-5 or Gemini 2.5 can now produce proofs that look convincing but turn out to be false. “They’re getting good enough to fool even experienced mathematicians,” Hayat warns.
To avoid this, his team works in formal languages such as Lean, Isabelle, and Coq, where each proof can be automatically verified by a computer. “If the computer says the proof is correct, then it is correct, 100 percent guaranteed,” he says. The drawback? Even less data to train on.
The same scarcity appears in mathematical discovery: for problems not yet solved, there are no examples to learn from. “We need inventive generation techniques,” Hayat explains. “We have to create the data before we can learn from it.”
Toward a new practice of mathematics
Despite the challenges, progress is accelerating. “AI is already changing mathematics,” Hayat notes. “Old conjectures are being disproved, new ones are emerging, and more mathematicians, Fields Medalists among them, are using AI tools in their research.”
(Some of the ongoing work from the DESCARTES project was recently mentioned in Le Monde, in an article exploring how far AI might go in challenging human mathematics, although the project itself is not explicitly cited).
In the near term, the DESCARTES project aims to augment mathematicians, not replace them:
- By suggesting promising conjectures and directions for exploration.
- By automating routine parts of proofs.
- By formalizing human-written proofs for reliable peer review.
The long-term impact could be transformative. Autoformalization, the translation of informal, human-written proofs into computer-verifiable form, might revolutionize how mathematical research is reviewed, published, and trusted.
“Ultimately,” Hayat says, “this could change the way mathematics is practiced.”
A two-way influence
Mathematics and AI have always been intertwined. AI systems rely on mathematical foundations, from calculus and linear algebra to probability and optimization. But the DESCARTES project hints at a reversal.
“Over the short term, AI will have the stronger impact on mathematics,” Hayat believes. “It’s already expanding what mathematicians can do. Over the long term, the relationship will become cyclical: better AI will help us discover better mathematics, and better mathematics will lead to more intelligent AI.”
That loop may take time to close, but its implications reach far beyond the blackboard.
The bigger picture
AI has beaten humans at games, mapped proteins, and written poetry. If it can learn to reason like a mathematician, it could help accelerate discovery across every domain that depends on rigorous logic, from physics to engineering to cryptography.
AI won’t take mathematics away from humans, it may simply change the way humans do it.
Stay tuned for more profiles of our 2025 chairs, highlighting their work in AI & Society, AI & Business, and AI & Science.