Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Agentic Proof Automation: A Case Study

Yichen Xu, Martin Odersky

TL;DR

The paper tackles the high cost of mechanized proofs by introducing agentic proof automation, where off-the-shelf LLM agents perform mechanical proof engineering under human guidance. Through a Lean 4 case study of System Capless (over 14,000 lines), the authors demonstrate an 87% task-success rate across 189 tasks, with only 16% needing human intervention, and they provide an interactive explorer and open-source mechanization for replication. Humans supply mathematical insight, theorem statements, and strategies, while agents search codebases, craft proof scripts, and repair proofs in response to prover feedback, showcasing a practical workflow that accelerates formal verification. The results reveal that agents are strong proof engineers but limited in creative reasoning, underscoring a division of labor and the potential to broaden formal-method adoption while highlighting areas for future tooling and benchmarking improvements.

Abstract

Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language models (LLMs) create new opportunities for proof automation: modern LLMs not only generate proof scripts, but also support agentic behavior, exploring codebases and iteratively refining their outputs against prover feedback. These advances enable an emerging scheme where LLM-based agents undertake most proof engineering under human guidance. Humans provide mathematical insight (definitions, theorems, proof strategies); agents handle the mechanical work of proof development. We call this scheme agentic proof automation. We present this scheme through a case study: mechanizing the semantic type soundness of a sophisticated formal system, System Capless, in Lean 4, comprising over 14,000 lines of code. Using off-the-shelf LLM agents with a single lightweight proof-checking tool, the agents completed 189 proof engineering tasks with an 87% success rate, only 16% requiring human intervention. The case study demonstrates that agents are capable proof engineers that substantially boost productivity, though they fall short in creative reasoning and still require human guidance in certain cases. We release an interactive explorer where readers can examine all agent interactions; the mechanization is open-sourced for experiments and extensions.

Agentic Proof Automation: A Case Study

TL;DR

The paper tackles the high cost of mechanized proofs by introducing agentic proof automation, where off-the-shelf LLM agents perform mechanical proof engineering under human guidance. Through a Lean 4 case study of System Capless (over 14,000 lines), the authors demonstrate an 87% task-success rate across 189 tasks, with only 16% needing human intervention, and they provide an interactive explorer and open-source mechanization for replication. Humans supply mathematical insight, theorem statements, and strategies, while agents search codebases, craft proof scripts, and repair proofs in response to prover feedback, showcasing a practical workflow that accelerates formal verification. The results reveal that agents are strong proof engineers but limited in creative reasoning, underscoring a division of labor and the potential to broaden formal-method adoption while highlighting areas for future tooling and benchmarking improvements.

Abstract

Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language models (LLMs) create new opportunities for proof automation: modern LLMs not only generate proof scripts, but also support agentic behavior, exploring codebases and iteratively refining their outputs against prover feedback. These advances enable an emerging scheme where LLM-based agents undertake most proof engineering under human guidance. Humans provide mathematical insight (definitions, theorems, proof strategies); agents handle the mechanical work of proof development. We call this scheme agentic proof automation. We present this scheme through a case study: mechanizing the semantic type soundness of a sophisticated formal system, System Capless, in Lean 4, comprising over 14,000 lines of code. Using off-the-shelf LLM agents with a single lightweight proof-checking tool, the agents completed 189 proof engineering tasks with an 87% success rate, only 16% requiring human intervention. The case study demonstrates that agents are capable proof engineers that substantially boost productivity, though they fall short in creative reasoning and still require human guidance in certain cases. We release an interactive explorer where readers can examine all agent interactions; the mechanization is open-sourced for experiments and extensions.
Paper Structure (34 sections, 4 equations, 4 figures, 1 table)

This paper contains 34 sections, 4 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Agentic Proof Automation By Examples
  3. Setup
  4. Models and Frameworks.
  5. Agent Tools.
  6. Workflow.
  7. A Brief Introduction to System Capless
  8. Examples
  9. Proof Script Development
  10. Proof Repair After Refactoring
  11. Answering Questions About the Mechanization
  12. Stating and Proving Standalone Properties
  13. Other Examples
  14. Patterns and Limitations
  15. Human Guidance Patterns
  16. ...and 19 more sections

Figures (4)

  • Figure 1: The human-agent-prover workflow. The human provides tasks and guidance. The agent generates proof scripts and refines them based on Lean's feedback, reporting success or identified obstacles back to the human.
  • Figure 2: Abstract syntax of System Capless.
  • Figure 3: Typing rules of System Capless.
  • Figure 4: Evaluation rules of System Capless.