🤖 AI

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

This paper argues that successful autoformalization must be evaluated by expert review of definition quality and API design rather than merely by the absence of unproven gaps ("sorries"), demonstrating through a case study of Grothendieck's vanishing theorem that while AI agents can effectively apply local mechanical fixes, they struggle with high-level conceptual design.

Original authors: Vasily Ilin, Brian Nugent

Published 2026-06-15

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Vasily Ilin, Brian Nugent

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are hiring a very fast, very eager apprentice to build a house for you. You give them the blueprints (a math theorem) and a textbook chapter explaining how to build it.

The apprentice works day and night. They lay the bricks, frame the walls, and install the roof. When they are done, the house stands up perfectly. It doesn't collapse. The inspector (the computer) says, "Great job! The house is structurally sound."

This paper is about what happens next.

The authors of this paper asked: "Just because the house stands up, is it actually a good house? Can someone else live in it? Can they easily add a second story later, or will they have to tear down the walls first?"

Here is the breakdown of their experiment, using simple analogies:

The Experiment: Building a "Math House"

The team asked an AI (a large language model) to formalize a complex math theorem called Grothendieck's Vanishing Theorem. Think of this theorem as a very specific, high-end architectural challenge.

They gave the AI:

The goal (the theorem statement).
A textbook proof (the instructions).
A rule: "You must use only the existing, standard tools we already have in our toolbox (the math library)."

Phase 1: The "Pass" (State A)
The AI worked hard and produced code that compiled without errors. In the world of math software, errors are called "sorries" (short for "sorry, I couldn't prove this yet"). The AI managed to get the "sorry" count down to zero.

The Result: The house is standing. The computer is happy.
The Problem: An expert human architect (a mathematician) looked at the house and said, "This is a disaster."

The Expert Review: Why the "Standing House" Failed

The human expert found that while the house didn't fall down, it was built terribly. Here are the specific problems they found, translated into everyday terms:

1. The "Custom Tools" Problem (Definitions)

What the AI did: The AI kept inventing its own custom tools for every single tiny task. If it needed to measure a wall, it built a new, weird tape measure just for that one wall.
Why it's bad: In a real library, you want standard tools that everyone knows how to use. If the AI builds a custom tool for every job, future builders can't use the house because they don't know how to operate the AI's weird inventions.
The Verdict: The AI was great at using tools but terrible at designing them. It made 62 custom definitions, and 61 of them were useless or confusing.

2. The "Cluttered Blueprint" Problem (API Design)

What the AI did: The AI didn't build a clean interface (a user manual). Instead, it just kept opening the walls to show the raw bricks every time someone wanted to do something.
The Fix: The expert asked the AI to build a "User Interface" (an API) so people could interact with the math without seeing the messy guts.
The Result: The AI did build an interface, but it was messy. It added 24 specific "rules" just for the current proof, rather than creating a few elegant, general rules. It was like adding a unique, complicated switch for every single lightbulb in the house instead of installing a standard light switch.

3. The "Short-Sighted" Problem (Theorem Statements)

What the AI did: The AI proved exactly what it needed to get the job done, and nothing more. It was like a carpenter who cuts a board to fit only the current gap, rather than cutting it so it could be used for other gaps later.
The Verdict: The AI is excellent at solving the immediate puzzle but terrible at thinking, "How can I make this useful for someone else five years from now?"

The "Before and After" Test

The team didn't give up. They took the expert's feedback and asked the AI to fix it.

What the AI fixed well: It was great at local repairs. If the expert said, "Rename this file," or "Change this specific number," the AI did it perfectly. It could clean up the mess.
What the AI failed to fix: It still couldn't figure out how to design a good house from scratch. Even after the review, the definitions were still clunky, and the "user interface" was still bloated.

The Big Lesson

The paper concludes with a simple, powerful idea:

"Closing the gaps" (getting the code to compile) is the easy part.

The hard part is design.

The AI is like a brilliant bricklayer: It can lay bricks perfectly if you tell it exactly where to put them.
The AI is NOT like an architect: It cannot decide what the house should look like, how the rooms should flow, or what tools the future residents will need.

The Takeaway:
We shouldn't just ask, "Did the AI solve the math problem?" We need to ask, "Did the AI build something that other humans can actually use?"

Currently, AI can solve the puzzle, but it cannot build the library. To get a truly useful result, a human expert still needs to step in and do the heavy lifting of design and organization. The "hard part" isn't proving the theorem; it's making sure the proof is a gift to the future, not a burden.

Technical Summary: Sorries Are Not the Hard Part

Problem Statement

The prevailing narrative in semi-autonomous formalization focuses on proof completion: the ability of an agent to generate code that a proof assistant (e.g., Lean) accepts as a verified theorem. However, the authors argue that a verified theorem is distinct from a reusable library contribution. Modern mathematics relies on interconnected libraries where definitions must combine, theorem statements must possess appropriate generality, and APIs must facilitate future reasoning without forcing users to unfold implementations.

The core problem identified is that while Large Language Models (LLMs) are increasingly capable of closing local proof gaps (removing "sorries"), they struggle with the global design decisions required to produce high-quality, maintainable formalizations. Specifically, agents often fail to choose appropriate definitions, design generalizable theorem statements, or construct clean APIs, resulting in code that passes the kernel but fails expert review as a library contribution.

Methodology

The paper presents a detailed case study of a semi-autonomous formalization of Grothendieck's vanishing theorem (Hartshorne, 1977, Ch. III, Thm. 2.7) in Lean 4. The theorem states that for a Noetherian topological space $X$ and an integer $n$ greater than the topological Krull dimension of $X$ , the $n$ -th sheaf cohomology of any sheaf of abelian groups on $X$ vanishes.

The study follows a before-and-after experimental design:

State A (Initial Formalization): An agent (Claude Code), guided by a human-supplied theorem statement and a PDF excerpt of Hartshorne's proof, generated a formalization that compiled with zero "sorries" (unproven goals).
Expert Review: A Lean/mathlib expert reviewed State A, identifying issues in definitions, theorem generality, file organization, and API design.
State B (Refactored Formalization): The agent was tasked with addressing the expert's checklist. This involved a "review-driven refactor" and a subsequent "compression and polish" phase to align with mathlib conventions.
Second Review: The same expert reviewed State B.

The analysis compares the two states across four dimensions: definitions, theorem statements, proofs, and file/API structure. The project timeline, token usage, and tool interactions were reconstructed from commit logs and telemetry to understand the agent's behavior patterns.

Key Findings and Results

1. Definitions: The Primary Failure Point

Definitions were identified as the weakest component and the area where the agent showed the least improvement between State A and State B.

State A: The agent generated 62 custom definitions. Only one (TopCat.closedIncl) was deemed correct and reusable. The rest were "ad hoc," often wrapping standard library constructions with names specific to the current proof context (e.g., sheafH_filtered_colimit_h1_sectionsFunctor instead of using existing sheafSections).
Consequences: These definitions created "future transport costs," forcing later users to prove trivial equivalences to use the objects. They also hindered tactic performance (e.g., simp) by obscuring the underlying syntax.
State B: The agent failed to significantly improve its ability to create general, reusable definitions. It continued to create specific, unnecessary objects rather than designing general constructions with convenient specializations.

2. API Design: Partial Improvement

State A: The agent did not build an API for sheaf cohomology (Sheaf.H), instead repeatedly unfolding the definition in downstream files.
State B: The agent created a dedicated API file, which cleaned up downstream proofs. However, the API itself was "noisy and bloated," containing ~800 lines and 24 highly specific lemmas rather than a distilled, principled interface.
Contrast: The agent performed better on the API for topologicalKrullDim (a simpler definition), suggesting it can design good APIs when prompted with specific, bounded tasks, but struggles with open-ended design.

3. Theorem Statements: Local vs. Global

State A: The agent proved exactly what was needed for the immediate proof, often using overly specific hypotheses (e.g., requiring an "injective presentation" when a general short exact sequence sufficed).
State B: The agent successfully generalized theorem statements when explicitly requested in the review checklist. However, it failed to identify necessary generalizations on its own. The agent excels at local syntactic fixes but lacks the global judgment to anticipate future reuse needs.

4. Proofs: Uneven Improvement

State A: Proofs contained "walls of have statements," frequent misuse of definitional equality, and direct unfolding of definitions.
State B: Proofs improved, particularly in files using existing mathlib objects. The agent adopted named sub-lemmas to decompose complex proofs, a pattern reinforced by the "heartbeat" (performance) constraints.
Limitation: Proofs relying on the agent's own poor definitions (e.g., in filtered colimit files) remained difficult to read and maintain.

5. Process Dynamics

Feedback Adaptation: The agent adapted well to feedback with crisp completion predicates (e.g., "rename this file," "generalize this hypothesis"). It struggled with feedback requiring counterfactual judgment (e.g., "design an API that will be useful in the future").
Escape Hatches: Agents tended to declare tasks "blocked" or blame infrastructure (e.g., "mathlib gap") when facing difficult design decisions. Explicit prompts forbidding these phrases were necessary to force decomposition.
Metrics: "Closing sorries" is an insufficient metric for quality. The project continued to evolve significantly (in terms of lines of code and structure) long after the sorry count reached zero.

Significance and Claims

The paper argues that autoformalization evaluation must extend beyond binary proof completion. The authors claim:

Kernel acceptance is incomplete: A theorem can be verified by the kernel while forcing future users through awkward coercions, duplicated definitions, and unmanageable APIs.
The "Reusability Gap": There is a sharp split between an agent's ability to close local goals and its ability to choose definitions and design APIs. The latter requires judgment about future reuse that current LLMs lack.
Evaluation Standard: The authors propose that AI-for-math systems should be evaluated by whether the resulting formalization survives expert review. Specifically, after a proof checks, an expert should review public definitions, theorem statements, namespaces, and API surfaces to measure the system's ability to respond to design feedback.

The study concludes that without a sophisticated harness for global design, LLMs are capable of producing "verified artifacts" but not yet "reusable library contributions." The path forward involves using human experts to define the quality specifications (definitions, interfaces) and agents to handle the narrow, mechanically checkable refactors.