Auto-Formalization

Auto-formalization is the process of turning informal mathematical text into formal definitions, theorem statements, and proofs that a system such as Lean Theorem Prover can check. In 137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的, Hong Letong / 洪乐潼 argues that this layer is underappreciated and may be at least as hard as theorem proving itself.

Key Claims

• Informal mathematical prose leaves definitions, assumptions, notation, and proof steps implicit; formal systems require those choices to be explicit.
• Without auto-formalization, an AI prover can be strong only on problems already converted into formal language.
• Auto-formalization expands Mathlib and the machine-readable knowledge base that an AI Mathematician can use.
• The same idea connects to Formal Specification in software: the system cannot prove code correct until the intended property has been precisely stated.

Connections

• AI For Math, Axiom, and Axiom Prover — source context for the concept.
• Lean Theorem Prover, Mathlib, and Interactive Theorem Proving — formal substrate and proof loop.
• Formal Verification, AI Verification, and AI Coding Verification — adjacent verification tasks that also depend on precise statements.