The checker finding mistakes in the thing it was checking.
Development
Gauss formalizes a Fields Medal proof and finds two errors in it
Claim
Math, Inc.'s Gauss completed the Lean formalization of Viazovska's Fields Medal-winning sphere packing proof in two weeks across more than 200,000 lines of verified code, catching two errors in the original arguments, with even sceptic Daniel Litt calling it the first truly autonomous formalization of a substantial result.
Reported metric: 2 weeks / 200,000 lines
Reporting date: (not necessarily the event date)
Sources
Attribution and reporting linked by this record; links do not imply independent verification.
- Welcome to March 3, 2026 (theinnermostloop.substack.com)
Cite or correct this record
Suggest a correction — opens a GitHub draft for you to review and submit.