# Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

> LLMs excel at closing proof goals but remain weak at choosing definitions and designing APIs, so autoformalization evaluation must shift from compilation success to expert review of library quality.

- **Source:** [arXiv](https://arxiv.org/abs/2606.13925)
- **Published:** 2026-08-22
- **Permalink:** https://picx.dev/p/vP8iCu
- **Whiteboard:** https://picx.dev/p/vP8iCu/image

## Summary

## 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:

```txt
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):

| Phase | Duration | What happened | Main difficulty |
|---|---|---|---|
| Formalization | Mar. 27–Apr. 4; nine active days | Claude Code followed the supplied Hartshorne proof plan, with Aristotle used for bounded lemmas. Produced state A, the first sorry-free version. | The agent could close local goals, but the emerging API was ad hoc. A heartbeat detour stopped clean compilation until large proofs were decomposed. |
| Expert review | Apr. 8–15; one week | The expert read the first verified tree as library code and wrote a structured audit with large cross-file changes and per-file comments. | The review judged code after kernel success, so it found design failures that no proof-completion metric could see. |
| Review response | Apr. 17–May 1; about two weeks | The main refactor loop ran Apr. 19–27. | Local checklist items were tractable; open-ended requests such as building a usable Sheaf.H API were much harder. |
| Compression and polish | Apr. 27–May 1 | Compression loop followed by mathlib-style cleanup for names, docstrings, lint, and stale comments. | The LOC gate found real redundancy, but short code was only a proxy for library quality. |

### 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:

| Review theme | State A criticism | State B outcome |
|---|---|---|
| File structure | File names were confusing and unorganized. | **Fixed.** File names make sense and docstrings became readable. |
| Definitions | Dozens of specific and often unnecessary definitions. | **Still the weakest category**, did not noticeably improve after the review. |
| Theorem statements | Most intermediate results were not general enough to be reusable. Agent proved exactly what it needed and nothing more. | All specific changes requested were done but the agent failed to identify further changes on its own. |
| API design | Proofs worked by repeatedly unfolding definitions rather than building an interface. | **Partially fixed.** Downstream files are cleaner but the API itself is noisy and bloated. |
| Proof style | Long walls of `have` statements and frequent misuse of definitional equality. | Better but uneven. Some files became maintainable; filtered-colimit files are still quite bad. |

### 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.

---

_Markdown view of https://picx.dev/p/vP8iCu, served by PicX — AI-generated visual whiteboard summaries of research papers._