In situ Formalization
Published:
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. OpenAI recently released over 700 AI-generated manuscripts on open problems, but three were withdrawn soon after their release, and the status of many claims is unverified. 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. Whether that statement means what the natural-language text claims lies outside the checker, and checking it remains a human task that does not scale with AI output.