Math Inc Autoformalization Projects
· updated
math · code · research
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.