Math, Inc. Autoformalization Projects
Five formalization results from my work at Math, Inc.
During my time at Math, Inc., we’ve published five autoformalization projects so far:
- Security of the FRI protocol
- Kakeya set problem over finite fields
- Riemann Hypothesis for hyperelliptic curves over finite fields
- Sphere packing in 8 and 24 dimensions
- Resolution of FrontierMath open problem on hypergraphs
These projects contain complete Lean 4 formalizations, generated by Gauss from provided LaTeX blueprints.