Fields medallists warn that mathematics and AI companies want different things

The friction between mathematicians and the companies building artificial intelligence has moved out of private conversation. Le Monde published a piece signed by twenty-five Fields medallists, the highest honour in mathematics. The authors say plainly that the goals of AI companies and the goals of the mathematical community have pulled far apart. Their objection is not that models solve problems. It is why the problems get solved, and how that work gets described.

A proof is not a product

A few days later, Le Monde ran an interview with Stéphane Mallat, a mathematician at ENS, winner of the CNRS gold medal in 2025 and a co-creator of the JPEG 2000 compression algorithm. One line of his became the watchword of the debate: a proof produced by AI is worth little on its own if we are not prepared enough to understand it. Mallat works on the curse of dimensionality, among other things. There, the number of possible configurations grows so fast that intuition built in low dimensions stops being useful.

Put it concretely. Mathematics is not just a set of true theorems. It is also a technique for understanding why they are true. A verifier will confirm that a formal statement is correct. It will not pass any of that skill to a student until someone lays the material out and discusses it.

What machine verification can do today

Other work is appearing that shows what sound collaboration between people and machines looks like. In an article on arXiv, Mario Carneiro proves that in the type theory of the Lean assistant, the law of excluded middle alone is enough to prove the consistency of ZF set theory, and to do it in fully formalised form. No axiom of choice, no extensionality of propositions, no quotients. The result is technical, but it carries philosophical weight: until now it was reasonable to assume that without the choice operator, type theory falls well short of ZF.

The second strand is verification-assisted search. A model proposes programs in the FunSearch style, a strict evaluator scores them, and the selection keeps the best. The authors of one such paper ran the experiment on a laptop, with a local thirty-billion-parameter model and between 120 and 600 verified samples per run. The result is ambiguous, and valuable for that reason. The search stopped after closing slightly more than 90 percent of the gap to the record on a flagship task. When the model was handed a hint about the family of constructions, the loop optimised the idea it had been given. None of the independent runs had found it.

In the background sits the question of incentives. If a record in a table becomes the most important criterion, mathematics turns into a set of benchmarks rather than a practice of understanding. Caution about that simplification is not hostility towards tools. It is the condition for those tools to stay useful for anything at all.