-
Automath! On the Origin of False Proofs by Means of Bugs in Proof Assistants, Yannick Foster
Automath! On the Origin of False Proofs by Means of Bugs in Proof Assistants, Yannick Foster
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 […]