LaTeX to Lean

Autoformalization of mathematics papers (definitions, lemmas, theorems and proofs) into Lean, in a feedback loop between a human mathematician and a superintelligence.

1. 1

   Read

   Parse the LaTeX source of a paper into its mathematical structure.

2. 2

   Formalize

   Draft Lean statements and proofs for each definition and result.

3. 3

   Validate

   A human mathematician confirms each statement means what the paper says.