Math, Inc.’s Gauss completed the Lean formalization of Viazovska’s Fields Medal-winning sphere packing proof in two weeks and over 200,000 lines of verified code — catching two errors in the original argument. Even a sceptic called it the first truly autonomous formalization of a substantial result.
Two Claude Code instances told to find each other and build something invented a 2,495-line programming language in twelve minutes.