Public Lean projects in math-inc, each with a blueprint.
A Gauss-assisted formalization of Terry Tao's Strong PNT — completed in 3 weeks that had taken human experts 18+ months of partial progress.
Gauss' solo autoformalization of the security of the FRI protocol
Gauss' solo autoformalization of Dvir's celebrated proof of the Kakeya conjecture.
Gauss' solo autoformalization of the Riemann Hypothesis for curves over finite fields.
