Summary of "Studying Proof Data with Proof Theory: The Case of AI-Generated Mathematics"

Summary (Overview)

• This paper presents a novel methodology for empirically analyzing large collections of formally verified mathematical proofs, treating proof-theoretic quantities as measurements of proofs rather than optimization targets.
• The author compiled 96 projects from OpenAI's AI-written mathematics library, three smaller AI corpora (sphere packing, Putnam 2025, IMO 2025 solutions), and two human research projects (Carleson, sphere eversion), all against the same version of mathlib (Lean's main library).
• Key findings: AI-generated proofs diverge significantly from human-written ones in structure—OpenAI's gesture mix is 5.8× farther from mathlib than random mathlib samples are from themselves, and AI proofs realize far less available logical compression (31% vs. 73% in mathlib).
• The paper introduces novel concepts: gestures (structure-preserving abstractions of proof steps), eigenproofs (directions of maximal divergence), and realized compression (the fraction of available sharing a proof actually exploits).
• Three main results survive all controls: (1) gesture-mix divergence, (2) excessive intermediate claims (40% of OpenAI proofs are larger with their cuts than without, vs. 13% in mathlib), and (3) low realized compression.

Introduction and Theoretical Foundation

Historical Motivation: Brahe, Kepler, and Newton

The author draws an extended analogy between the Scientific Revolution and the current state of AI-generated mathematics. Just as Tycho Brahe's meticulous astronomical observations provided the data that enabled Kepler's laws and Newton's synthesis, the author argues that large collections of formally verified proofs constitute "mathematical data" that can be turned into "mathematical evidence."

Key historical innovations cited:

• Kepler's five evidentiary innovations: using the true sun rather than the mean sun, bisection of eccentricity, the area rule, and the elliptical orbit model
• Newton's synthesis: showing that mathematical structures underlying celestial and terrestrial mechanics could be systematically related

"The transition to Newtonian mechanics thus depended on a methodological transformation in which observations were systematically collected, discrepancies were treated as grounds for revising existing models, and mathematical relationships were used to establish connections that the observations alone could not have revealed."

The Foundational Crisis

The paper reviews the 19th–20th century foundational crisis through the lens of two opposing attitudes:

1. Kronecker's finitism: "God made the integers, all else is the work of man" — mathematics must be grounded in finite, constructive processes
2. Cantor's freedom: "Mathematics is completely free in its development and is only bound to the self-evident consideration that its concepts are both free of contradictions..."

The author traces how these attitudes played out through Frege, Hilbert, Borel, Brouwer, and Heyting, culminating in Gentzen's proof theory.

Proof Theory: Natural Deduction and Cut Elimination

The paper presents Gentzen's sequent calculus (LJ) and the cut elimination theorem in detail. Key rules include:

Sequent form: $\Gamma \vdash A$

Cut rule:

$$\frac{\Gamma \vdash A \quad \Delta, A \vdash C}{\Gamma, \Delta \vdash C} \text{(Cut)}$$

Cut elimination theorem: Every derivable sequent in LJ has a cut-free derivation.

The rank of a formula is defined by:

$$r(P) = r(\bot) = 0$$ $$r(A \circ B) = 1 + \max\{r(A), r(B)\}, \quad \circ \in \{\land, \lor, \to\}$$ $$r(Qx\,A) = 1 + r(A), \quad Q \in \{\forall, \exists\}$$

Boolos's "Don't Eliminate Cut"

The paper invokes Boolos's (1984) argument that while cut elimination is possible in principle, the cut-free derivation can be unimaginably large. This motivates measuring whether cuts earn their place in actual proofs.

Methodology

Proofs as Programs (Curry–Howard)

Lean rests on the Curry–Howard correspondence: propositions are types, proofs are programs. The paper distinguishes between:

• Source text: what a person or machine types (tactics)
• Proof term: the kernel-checked program that the tactics elaborate

Gestures

Definition: A gesture is a proof term node with three transformations:

1. All hypothesis names erased
2. Every type reduced to its head connective (e.g., $=$ for equations, $\to$ for implications)
3. Each hypothesis labeled by usage count: 0 (never), 1 (once), or $\omega$ (more than once)

For example, every use of transitivity of equality becomes: Eq.trans (=, =) ⇒ =

Data Pipeline

1. Text study: 5-gram interpolated Kneser–Ney language model trained on mathlib's source; measures "energy" in bits per token
2. Compiled study: All corpora compiled with Lean 4.34.1 against mathlib at commit d13f23b
3. Hashing pass: Eliminates cuts by substitution, uses hash-consing to compute exact sizes of cut-free forms without materializing them

Cut Measures

For each proof $\pi$, three sizes are computed:

• $|\pi|$: size as written
• $|\pi^{cf}|$: size of cut-free form
• $|\pi^{opt}|$: size with optimal layout (keeping only cuts that save space)

Key definitions (all in bits):

Cut compression:

$$\kappa(\pi) = \log_2 \frac{|\pi^{cf}|}{|\pi|}$$

Compressibility:

$$\chi(\pi) = \log_2 \frac{|\pi^{cf}|}{|\pi^{opt}|}$$

Layout redundancy:

$$\rho(\pi) = \log_2 \frac{|\pi|}{|\pi^{opt}|}$$

These satisfy: $\kappa = \chi - \rho$

The five normal forms split $\kappa$ into:

$$\kappa = \underbrace{\log_2 \frac{N_3}{N_2}}_{\sigma} - \underbrace{\log_2 \frac{N_1}{N_2}}_{\ell} - \underbrace{\log_2 \frac{N_0}{N_1}}_{w}$$

where $\sigma$ is the gain from shared cuts, $\ell$ the cost of naming proofs used once, and $w$ the cost of never-used proofs.

Realized Compression

For cut-free proof size $S$, define:

• $\chi^{author} = \log_2(S/A)$: what the author's cuts achieve
• $\chi^{lb} = \log_2(S/G)$: an explicit layout naming any repeated subproof that pays for itself
• $\chi^{DAG} = \log_2(S/D)$: full sharing with no naming cost

Realized share: $\frac{\sum_\pi \chi^{author}(\pi)}{\sum_\pi \chi^{lb}(\pi)}$

Control Measures

The paper implements several controls:

• Null distributions: random size-matched samples of mathlib against itself
• Automation controls: proofs with no tactic calls, certificates collapsed to single steps
• Layout controls: proofs in optimal layout ($\rho = 0$), proofs with no cuts
• Compilation controls: shared vs. module-by-module environments

Empirical Validation / Results

Text Energy

76% of the gap comes from identifiers (names); syntax adds only 0.28 bits.

Gesture Divergence

• OpenAI's gesture mix: 280 bits from mathlib
• Null (random mathlib samples): 49 bits (max 58 in 10 draws)
• Ratio: 5.8×

The first four eigenproofs:

Basic Step Statistics (medians over projects)

Cut Statistics

OpenAI's redundancy $\rho$ is higher than mathlib's (AUC 0.95, $p = 2 \times 10^{-44}$) and higher than human research code's (AUC 0.85, $p = 4 \times 10^{-5}$).

Realized Compression

Tooling Controls

With automation collapsed, OpenAI's divergence falls from 280 to 182 bits (3.7× null); with rewriting also collapsed: 191 bits (3.4×); on author's own steps only: 220 bits (3.9×).

On proofs calling no automation:

On no-automation proofs: mathlib realizes 86%, human research 82%, OpenAI 55%, sphere packing 33%.

Instrument Checks (Rank Ladder)

The paper verifies that created redexes can only arise from cuts of rank ≥ 1. Initial failures revealed two instrument bugs (syntactic rank reading, missed cuts behind substitutions). After fixes, the ladder holds for every proof with created redexes in every corpus (1,100 in mathlib).

Theoretical and Practical Implications

Theoretical Contributions

1. Proofs as measurable objects: The paper demonstrates that proof-theoretic quantities (cut structure, compression, redundancy) can serve as empirical measurements, not just optimization targets.

2. The gesture abstraction: Provides a way to compare proofs of entirely different theorems by stripping away content while preserving structure.

3. The tension between Cantor and Kronecker: The author frames the methodology as navigating between Cantorian freedom (abstracting away content to find common structure) and Kroneckerian constructivism (insisting on the actual construction, the kernel-checked proof term).

Practical Implications

1. For AI prover development: The low realized compression of AI proofs suggests concrete improvement targets—writing fewer dead intermediate claims and better exploiting repeated subproofs.

2. For formal verification practice: The paper highlights the importance of tracking compilation failures and provenance; 67% of IMO solutions failed to compile against the target mathlib version.

3. For the "Navier–Stokes" controversy: The author cites Bastounis et al. (2026) showing discrepancies between informal claims and formalizations, arguing that empirical proof analysis can help identify artifacts requiring closer inspection.

4. For mathematical archiving: The author envisions "a mathematical archive in which failures and corrections remain visible, so that accumulated proofs become a resource for discovering regularities."

Conclusion

The paper's central findings:

1. AI-generated proofs have a measurably different structure from human proofs, even after controlling for tooling and layout
2. AI proofs are redundant: 40% are larger with their intermediate claims than without them
3. AI proofs realize less available compression: 31% vs. 73% in mathlib (55% vs. 86% without automation)

The author acknowledges limitations: mathlib is a polished library with a house style; the gesture study doesn't control for subject matter; the human research reference is small.

Future directions:

• Measuring abstraction (cut introduction) at scale, not just repetition
• Testing whether current categories "collapse under closer inspection"
• Building archives where failures remain visible
• Extending the methodology as corpora grow

The paper concludes with a Lakatosian perspective: "the proof is a moving object, altered by criticism, counterexample, and the introduction of distinctions that were invisible in the original formulation." The empirical study of proofs is "a rather peculiar science, whose data are themselves mathematical constructions and whose instruments must answer to mathematical theorems."