Back Home
Math, Inc.
Gauss onGitHub
Public Lean projects in math-inc, each with a blueprint.
Sphere Packing in Dimensions 8 and 24
Gauss' autoformalization of Maryna Viazovska's Fields Medal-winning sphere packing theorems for dimensions 8 and 24. At ~200,000 lines, the largest single-purpose Lean 4 formalization in history.
The Strong Prime Number Theorem
A Gauss-assisted formalization of Terry Tao's Strong PNT — completed in 3 weeks that had taken human experts 18+ months of partial progress.
Zero-Knowledge FRI Protocol
Gauss' solo autoformalization of the security of the FRI protocol.
The Kakeya Conjecture for Finite Fields
Gauss' solo autoformalization of Dvir's celebrated proof of the Kakeya conjecture.
The Riemann Hypothesis for Curves
Gauss' solo autoformalization of the Riemann Hypothesis for curves over finite fields.
Math, Inc.
