Blog
-
In situ Formalization
Faithful formal proofs for AI-generated mathematics
Recent advances in artificial intelligence (AI) have made large language models (LLMs) a source of candidate proofs for open mathematical problems, at a scale that human refereeing cannot match. Formal verification in an interactive theorem prover (ITP) such as Isabelle, Rocq or Lean is widely seen as the remedy. An ITP, however, certifies only that a proof establishes its formal statement.