Math, Inc. Autoformalization Projects
Three formalization results from my work at Math, Inc.
At Math, Inc., I’ve published three autoformalization projects so far:
- Security of the FRI protocol
- Kakeya set problem over finite fields
- Riemann Hypothesis for hyperelliptic curves over finite fields
These three repositories contain complete Lean 4 formalizations, generated by Gauss from provided LaTeX blueprints.