HumanLean

Faithful Lean proofs, made for human review

Yuhao Mao, Chenhao Sun, Yani Zhang, and Martin Vechev

AI-generated mathematics is increasingly accompanied by AI-generated Lean formalizations. Existing formalization agents optimize for compilation, but compilation alone does not guarantee faithfulness to the original argument, and unfaithfulness undermines the correctness guarantee that formalization is meant to provide. We introduce HumanLean, the first system designed to produce compiling, faithful Lean proofs for human review.

Unfaithfulness is widespread

We found widespread unfaithfulness in formalizations from OpenAI’s recent advances, Axiom’s Stacks project, and various projects listed on Papers with Lean. This significantly undermines the correctness guarantees for the original mathematics.

Navier–Stokes

In the formalization accompanying OpenAI’s Navier–Stokes proof, we identify 24 numbered results with substantive differences. These include 3 with statement or mathematical-object differences and 21 with proof-argument differences.

Read Navier–Stokes audit PDF

Quasi-Riemann

In the formalization accompanying OpenAI’s Quasi-Riemann proof, we identify 9 numbered results with substantive differences. These include 4 with statement or mathematical-object differences and 8 with proof-argument differences.

Read Quasi-Riemann audit PDF

Axiom Stacks

Across five foundational chapters of Axiom Stacks, we identify 94 definitions and results with substantive differences: 6 definition mismatches, 1 statement mismatch and 88 proof replacements.

Read Axiom Stacks audit PDF

Various Formalizations on PapersWithLean

We found substantive differences in mathematical statements or proof arguments in 29 AI-assisted formalizations listed on Papers with Lean.

Explore findings in 29 formalizations

Formalization	Statements and definitions	Proof arguments
An orthogonality inequality in RP^{n-1} and the double-cap conjecture	-	Proposition 3.4 (concavity; separate proof): The paper derives concavity from unions and intersections of rotated sets. The Lean proof instead uses an elliptic maximum principle to make an affine contact constant along a compression path, then derives the chord inequality.
A curved three-dimensional simplex Hilbert transform	-	Bounds (2.4), (2.11): main theorem exponent range: The paper controls translated kernels using shifted maximal functions with polynomial frequency loss. In the main theorem exponent range, the formal proof replaces this with adjustable exponential-loss and loss-free low-pass estimates, then chooses interpolation parameters to recover decay. · Evidence 2
Ternary polynomial relations and periods of cusp forms	-	Proposition C.1: The paper obtains coercivity from a uniform spectral gap for irreducible unitary representations and a direct-integral decomposition. The formal proofs instead establish finite-dimensional coefficient-Hodge positivity and combine it with an integrated energy identity. · Evidence 2
Certifying non-existence of integer points on curves	-	Octic certificate: local vanishing and local-value arguments: The paper proves outside-S vanishing using regular proper models and local constancy using the Tate pairing. The formal proof obtains the needed integer-candidate Hilbert sums from eighth-power identities and finite residue covers. · Evidence 2
Higher derivatives of the Gram function	Auxiliary asymptotic assertion after (11), α_part_expansion: The paper’s expansion fixes one remainder identity on a tail. The exported lemma instead permits a new remainder for each input and constrains it only there; its proof nevertheless constructs a uniform remainder.	-
Baire measurable functions and automorphisms of the truth-table degrees	-	Proposition 4.8: The paper obtains inverse regularity through generic meets and definability of the degree graph. The formal proof instead uniformizes reduction triples on a product space and removes an auxiliary oracle in both directions, bypassing that graph argument.
Strict Dirichlet Pólya Inequality for Simply Connected Planar Domains	-	Resonance/pole step (Lemma 4.1; alternative proof): The paper creates a pole on fixed boundary data by isolating a small spectral cluster in the resolvent. The formal proof instead restricts resonant eigenfunctions to moving inner boundaries and uses their first-order trace expansion and a positive Gram limit.
Coarse ellipticity and De Giorgi-Nash-Moser theory in the optimal range	-	Lemma 9.6: The paper reconstructs the function with whole-space Newtonian potentials and bounds each block by splitting the kernel near and far. The formal proof uses zero-boundary cube Dirichlet blocks and obtains the supremum bound from local Morrey and gradient estimates.
Associativity of Multiplication Is Hard for Resolution	Definition A.2 (Wallace circuit): The Wallace circuit groups different partial products in its first adders, changing the internal circuit/CNF rather than merely renaming its wires.	-
A Proof of the Linear Hadwiger Conjecture	-	Augmentation argument (final-paper Lemma 7): The paper bounds incident dual penalties at every vertex by perturbing an optimal dual solution. The formal argument instead controls total penalties and excludes a small heavy-vertex set from the augmentation, paying for it in the coloring error.
Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)	§2 pattern-substitution definition (unnumbered): General element substitution can capture a free set variable under μ/ν, changing the pattern’s denotation; the paper requires capture-avoiding substitution.	-
Total Variation Distance Estimation through Domain Reduction	Theorem 4.1 (circuit operation-count contract): The paper bounds total arithmetic work, including evaluation of the input circuits. The formal bound instead measures a cost that is zero at leaves and charges only sparsifier calls at internal nodes, so it bounds a different operation count.	-
The Exact Growth Rate of Space-Optimal Reversible Pebbling on Chains	-	Theorem 1.3 (complete-rate lower bound): The paper transfers the reach-cost rate to complete computations by counting merged marginal streams. The full-rate formal proof instead forces a single long reach component by a capacity argument and applies a single-row dispersion bound; marginal-stream results are also proved separately.
Variational properties of Perron's extremal solutions in the Bernoulli one-phase problem	-	Proposition 6.1: The paper preserves the subsolution property through an increasing family of shifted limits. The formal proof instead derives it from the final limit’s inner-variational structure, avoiding that monotone-stability argument.
The exact asymptotic constant in the metric dimension of Jaccard space	-	Table 1: β(2), β(3) minimality: The table reports exhaustive search for the small metric dimensions. The formal minimality proof instead constructs, for every possible single landmark, two sets with equal Jaccard distance; the upper-bound witnesses still use finite computation.
A counterexample to Köthe's conjecture and a question of Rowen	-	Proposition 2.4 (nonnilpotence): The paper rules out a polynomial right inverse by finite bandwidth, then uses that obstruction to prove the companion matrix nonnilpotent. The formal proof instead constructs an infinite-sequence eigenvector over k(t) and gives the companion matrix a nonzero eigenvalue.
Order closure, order adherence and Fatou norms	-	Proposition 2.4: The paper obtains its generator lower bound by covering the index set with finite sets in a c₀-controlled Banach lattice. The formal proof instead uses growing strips in a full function lattice and a diagonal obstruction to small generating families.
Common neighbour conjectures for Saxl graphs fail at every base size	-	Lemma 6.1 (irreducibility): The paper uses translation characters over F₄ and Clifford transitivity to prove irreducibility. The formal proof instead computes a rank-three commutant and rules out nontrivial idempotents with a concrete Paley-operator calculation.
On a conjecture on the Kasami APN function: reductions, structure theorems, a proof for k mod n∈{1,2,n−2,n−1}, and exhaustive verification for n≤ 13	Theorem 6.1 (auxiliary Walsh identity): The displayed identity Wψ(1,μ)=2S(μ) includes μ=0, whereas the formal statement requires μ≠0: at zero the two sides are 0 and 2^n. The principal correlation reduction and full Walsh Fourier formula are unchanged.	Lemma 11.1 (radical-dimension parity): The paper obtains radical-dimension parity from the even rank of an alternating form. The formal proof instead uses Parseval to obtain a nonzero integer Gauss-sum square and infers parity from its prime exponents.
A lower bound for stepsize-based acceleration of gradient descent	-	Lemma 5.3, (39): For (39), the paper optimizes the pairing and uses reverse Chebyshev; the formal proof instead factors a pointwise bound for ψ and applies AM–GM separately to two products. This bypasses the optimization and covariance step; (40) uses the same combination argument as the paper.
Maximally entangled states are not complete for pseudo-telepathy	-	Theorem 1.1 (finite-dimensional negative half): The paper invokes a tracial model with globally commuting Alice/Bob effects. The formal proof instead uses noncommuting matrix moments and derives zero products only for losing pairs, changing the feasibility argument used by the certificate.
Counterexamples to Schiffer's Conjecture	-	Theorem 2.7; Proposition 4.5: The lift replaces abstract Dirichlet solvability and weak-solution regularity with an explicit Fourier–Bessel field and second-jet matching. Near-integer crossings use simultaneous two-phase alignment rather than the paper’s one-dimensional irrational-rotation argument. · Evidence 2
Settling the Optimal Exponent Relating Sumsets and Difference Sets	-	Theorem 1.1: The paper’s witness uses carry-automaton counts and a cyclic additive basis in a CRT construction. The formal proof instead combines a base-39 gadget admitting direct product bounds with quadratic-row sum witnesses.
Record compositions of alternating permutations and noncommutative symmetric functions	NSym model (§5.1; Corollary 5.2): The NSym model adds an independent zero-indexed raw generator while defining Ψ₀=1. Its designated positive Ψ-generators therefore no longer generate the whole algebra, unlike the paper’s NSym model.	-
Four-digit Kaprekar dynamics in odd bases	-	Lemma 3.1 (surjectivity proof): The paper constructs a preimage by selecting signed half-coordinates and applying the inverse coordinate map. The formal proof instead builds a separate reverse injection from odd representatives and forces surjectivity by finite cardinality.
A problem of Andrews and Dhar on partitions	-	Proposition 3.15 (injectivity argument): The paper reconstructs the original partition by reversing its deletions. The Lean proof instead combines its right-inverse with Glaisher equicardinality of finite weight slices, giving a different argument for the same bijection.
Core Existence in Approval-Based Committee Elections with up to Seven Voter Types	-	Lemma 4.4 (four-voter branch): The paper excludes a common voter by rounding a reduced election, padding the integral committee and lifting it back. The Lean four-voter branch instead projects four incomparable approval types onto three voters and uses the antichain bound 4≤3 to obtain a contradiction.
Gaps in Multiplicative Sidon Sets	Lemma 3.3 (sieve axiom): The paper’s sieve estimate assumes δ>0. The formal axiom drops this condition and admits negative-δ inputs whose promised count exceeds the total possible number of prime pairs; its main application still chooses δ>0.	-
Taut fillings	Clean/normal vertex-link connectivity definition (§6): The paper requires connectivity inside the actual vertex link, whereas the formal graph permits paths through the removed vertex. Two tetrahedra meeting only at that vertex therefore satisfy the formal predicate despite a disconnected actual link; the stronger shelling conclusions are not refuted by this example.	-

Easing human review of formalizations

Unguided faithfulness

With HumanLean (powered by GPT-6-Astra), we observed 100% faithfulness in both statements and proofs across our evaluation of 12 publications and the unit-distance proof without human guidance. High unguided faithfulness reduces the chance of human intervention and thus reduces expected workload.

Compositional formalization

HumanLean proves internal results and exposes external results as explicit axioms. This division is more natural and manageable for human readers.

Minimal formalization

Compared with a raw agent instructed to do the same compositional formalization, HumanLean uses roughly 90% fewer custom definitions per formalized goal across both benchmark models, with fewer axioms and duplicate encodings. A minimal formalization reduces reading difficulty and improves reusability.

Raw agentHumanLean

Counts per formalized goal (lower is better). Duplicates are overlapping definitions of the same concept.

Interestingly, the stronger Astra model produces more definitions and duplicates per formalized goal in the raw-agent baseline. In HumanLean, it reduces verbosity, producing fewer definitions, proof declarations and duplicates per goal.

Example: a faithful unit-distance proof formalization

A formalization can change a statement, replace an argument, or assume a result the original proof sets out to establish. Thus, an unfaithful formalization cannot establish the correctness of the original proof, even if it compiles.

We formalize the unit-distance proof by OpenAI and compare our formalization with three other publicly available AI-assisted formalizations (plby, Logical Intelligence, and fbundle).

Importantly, we found all three compared formalizations unfaithful to the original proof.

	HumanLean	plby	Logical Intelligence	fbundle
Unfaithful statement	None found	Theorem 2.3Requires a stronger geometric condition.	None found	Lemma 2.6Weakens the packing bound.
Unfaithful proof	None found	Prop. 3.2 Prop. 3.8Uses a different field-tower construction.	Prop. 3.2Replaces the discriminant argument. Lemma 2.6Replaces the norm argument with a root-of-unity argument. Prop. 3.7 / A.13Replaces the divisor-sum argument with a zeta-function bound.	Props. 3.2 / 3.8Assumes the internal field-tower construction.

HumanLean: 4,618 subtotal / 4,618 total lines; plby: 14,647 subtotal / 975,620 total lines; Logical Intelligence: 8,615 subtotal / 31,501 total lines; fbundle: 4,021 subtotal / 5,805 total lines.

Subtotal sums definitions, assumptions, results/proofs and helpers, excluding external/background code. fbundle’s smaller subtotal reflects omitted formalization of a significant part of the proof, which is assumed as an axiom.

Explore all 25 Lean files

Find a file

Lines exclude blanks and all comment-only lines, including block/doc comments. Gutter numbers are source positions.

Formalization/Main.lean

Fold proofs

Download Lean project (.zip)

More to come

We are extending evaluation to more important AI-generated proofs and will later open-source HumanLean. Our manuscript is currently under review.