Summary (Overview)

• This paper presents a detailed case study of semi-autonomous formalization of Grothendieck's vanishing theorem in Lean, comparing an initial AI-generated formalization (state A) with a version refined through expert review (state B).
• The central finding is a sharp split in agent capabilities: LLM agents excel at closing proof goals and making local, mechanically checkable fixes, but remain weak at choosing definitions and designing APIs — the global design decisions that determine whether formalized code becomes a reusable library contribution.
• The agent produced 62 of its own definitions in state A, of which exactly one (TopCat.closedIncl) was judged to be of library quality; the remaining 61 were too specific, poorly named, or duplicated existing mathlib content.
• The paper argues that autoformalization evaluation should shift from "does it compile?" to "does it survive expert review?", proposing a practical evaluation standard based on expert review of public definitions, theorem statements, namespaces, and API surface.
• The project timeline shows the formalization phase was fast (9 active days), but the subsequent review-driven refactor (2 weeks) and compression/polish phases were essential for producing maintainable code — the sorry count reaching zero was not the end of the project.

Introduction and Theoretical Foundation

The paper addresses a fundamental gap in the evaluation of LLM-based formalization systems. While the default public story for semi-autonomous formalization is proof completion — can an agent produce code accepted by a proof assistant? — the authors argue this is insufficient. Modern mathematics is highly interconnected, and a formal library that supports it must be composable: definitions must combine, theorem statements must have the right generality, namespaces must support search, and APIs must let future users reason about properties rather than unfold implementations.

The case study centers on Grothendieck's vanishing theorem (Hartshorne, 1977, Ch. III, Thm. 2.7): if $X$ is a Noetherian topological space and $n$ is above the topological Krull dimension of $X$, then the $n$-th sheaf cohomology of any sheaf of abelian groups on $X$ vanishes. The Lean statement uses only existing mathlib definitions:

theorem GrothendieckVanishing
  (X : TopCat) [NoetherianSpace X]
  (n : Nat) (h : n > topologicalKrullDim X)
  (F : Sheaf AddCommGrpCat X) :
  Subsingleton (Sheaf.H F n)

This design choice matters: it prevents the agent from making custom definitions to render the theorem trivially true. The proof follows Hartshorne's route by induction on topologicalKrullDim X, requiring reductions through closed-immersion short exact sequences, irreducible components, flasque sheaves, extension by zero, and filtered colimits — all of which needed supporting definitions and API not currently in mathlib.

The paper's contributions are:

1. A case study of semi-autonomous formalization of a graduate-level algebraic geometry theorem in Lean
2. A qualitative before-and-after analysis of expert review feedback on definitions, theorem statements, proofs, and file/API structure

Methodology

Experimental Setup

The authors supplied Claude Code with a PDF excerpt of Hartshorne's proof and instructed the agent to follow that proof. The project was treated as a before-and-after experiment:

• State A: The first verified version, inspected by a Lean/mathlib expert
• State B: The version after an automated response to that review and a later mathlib-style cleanup, inspected by the same expert

Process Timeline

The project unfolded in four phases (Table 1):

Evaluation Framework

The expert review evaluated code along three main components: definitions, theorem statements, and proofs. The analysis distinguished between review items with a local syntactic target (which agents handle well) and items requiring global API judgment (which agents handle poorly).

Empirical Validation / Results

Quantitative Overview

The project involved substantial computational resources:

• 904 commits across the project timeline
• 31,529 turns in 270 sessions of Claude interaction
• 19,393 tool calls, dominated by shell/file operations and Lean LSP queries
• Total Claude usage cost approximately **$13K**, dominated by cache reads (about$10K)

The heartbeat episode (Mar. 28 – Apr. 1) illustrates a key failure mode: mathlib's synthInstance budget for HasDerivedCategory kept colliding with proofs, and the agent's first instinct was to raise set_option maxHeartbeats, oscillating budgets between 200K and 12.8M without producing a stable project. The episode only ended when an author instructed the agent to "keep optimizing until the whole project compiles with default heartbeats." The durable rule: never raise maxHeartbeats above 200000 — a proof too expensive to check is usually a proof that should be decomposed.

Qualitative Before-and-After Results

Table 2 summarizes the expert review findings:

Specific Definition Failures

The worst offender was sheafH_filtered_colimit_h1_sectionsFunctor — a definition equivalent to sheafSections (already in mathlib) with a name misleadingly suggesting connections to sheafH, filtered colimits, and H1. Such superfluous definitions are actively harmful: if instances (e.g., additive functor) are placed on them, they may not be definitionally equal to the standard instances, leading to confusing errors where rewriting works but instances break.

Other problematic patterns included:

• extClass_postcompAddEquiv_of_subsingleton_middle, sheafH_extClassAddEquiv_of_subsingleton_middle, and sheafH_succ_iso_of_subsingleton_middle — hyper-specific bijections that should have been proven as lemmas and used via Equiv.ofBijective
• sheafH0EquivSections and sheafH0NatIsoSections — essentially the same definition under different names
• familyMap — just Sigma.desc f, saving exactly one character of typing
• TopologicalSpace.IrreducibleCloseds.height — defined as a def instead of an abbrev, making all mathlib theorems about Order.height unusable without explicit unfolding

What Improved vs. What Persisted

Improved reliably:

• Local theorem generalizations (e.g., replacing "short exact sequence from an injective presentation" with just "short exact sequence")
• File organization and naming
• Proof style in files using mathlib's existing API
• Building a cohomology API file that contained the ad hoc proofs (though the API itself was bloated)

Persisted failures:

• Choosing the right level of generality for definitions
• Identifying which definitions should be public vs. private
• Building a small, principled API rather than accumulating 24 lemmas in a documentation header
• Making global design decisions that anticipate future use

Theoretical and Practical Implications

Why Definitions Matter

The paper argues that bad definitions create future transport costs. If a construction is placed at the wrong level of generality, later users must compare it to the version they actually need and transport every relevant theorem across that comparison — often harder than redoing everything from scratch. The finitely generated subsheaf construction is representative: the agent defined it for sheaves of abelian groups on topological spaces, but the construction is not inherently about either — a human library designer would design the general construction and provide convenient specializations.

The Nature of Feedback Adaptation

The authors identify why adaptation is uneven:

"The successful review items had crisp completion predicates: no remaining uses of an old name, a file renamed, a theorem statement generalized, a wrapper deleted, or a stronger isomorphism available at a call site. The failed items required counterfactual judgment."

A good definition is good because future developments can use it without transport pain. A good API is good because it contains the right small set of lemmas, including lemmas whose need has not yet appeared. The agent optimized for the next compiling proof but was unable to make good long-term decisions.

The Role of Gates and Escape Hatches

Two important practical findings:

1. Prompts must forbid escape hatches: The project's prompts explicitly forbade declaring tasks "blocked" or blaming infrastructure ("genuine mathlib gap") — "You are NOT allowed to say that you are blocked. You MUST close the sorrys yourself!" and "A no-op cycle is never acceptable."
2. Gates are only as good as their target: The compression loop (reducing normalized LOC under a compilation gate) was a reliable optimizer but only loosely aligned with review intent. Compilation gates are correctness gates; LOC and deadcode gates are maintenance proxies; review-item checklists are alignment proxies. None measures whether the public definitions are the ones a future formalizer would choose.

Conclusion

The paper concludes that without a sophisticated harness, LLMs are very capable of closing proofs and making local changes, but cannot yet make the global design decisions that a reusable formalization requires. Choosing good definitions and building good APIs remain the biggest barriers to AI-generated formalizations becoming reusable library contributions.

The authors propose a practical evaluation standard for AI-for-math systems: after the proof checks, ask an expert to review the public definitions, theorem statements, namespaces, and API surface, then measure how well the system responds. This shifts the evaluation target from kernel acceptance to library quality.

Future Directions

The findings suggest a division of labor for effective human-AI collaboration:

• Expert reviewers should spend their scarce attention on definitions, theorem surfaces, and global organization
• Agents should be handed narrow refactors that carry an explicit completion predicate

The code and data are publicly available: the Lean 4 formalization at GitHub and the full process logs (token usage, loop histories, tool-use timelines, prompts, and reviews) as a public dataset on Hugging Face.