Proof assistants have entered mainstream mathematical discourse so fast that now they are almost silently accepted as the ultimate guardians of correct proofs. Both the recent forced Euler blowup result by Buckmaster and Alpöge and the solution to the Navier-Stokes problem announced by OpenAI come with proofs verified in the Lean proof assistant, with code almost entirely written using LLMs. Only six months ago an experiment led by Tristan Stérin showed that LLMs are effective at finding bugs in proof assistants: several bugs were found both in Lean and the […]

À qui appartiennent les mathématiques ? En deux ans à peine, les mathématiques semblent être passées du statut de frontière de l’IA à celui de territoire de l’IA, du statut d’idéal cognitif servant à tester les capacités de raisonnement des modèles d’IA, à celui d’infrastructure de connaissance, productive et mobilisable de façon en partie automatisée. C’est en tous cas le message envoyé par OpenAI (e.g. Contre-exemple à la conjecture d’Erdős), Anthropic (e.g. Contre-exemple à la conjecture jacobienne), Google DeepMind (e.g. AlphaProof) ou encore la DARPA avec le programme ExpMath. Si […]