ProofBench v1.1

Key Takeaways

Claude Opus 5 leads ProofBench at 99%, followed by Claude Fable 5 at 95% and Kimi K3 at 87%, then Harmonic’s Aristotle at 86% and GPT-5.6 Sol at 83%.
Foundation models are improving on formal math: general-purpose models now surpass the specialized Aristotle system on this leaderboard.
Strong performance is not the same as good value: Claude Fable 5 costs $5.24 per task, roughly 2.9× Claude Opus 5, which scores higher. (Aristotle runs on Harmonic’s own infrastructure, so no cost is recorded for it.)
Nor is it the same as speed: Kimi K3 is among the cheaper models on the board at $1.65 per task, but averages 2,033 seconds per problem — 3.4× Claude Opus 5, which scores 12 points higher. Qwen 3.8 Max is comparable at 1,863 seconds.

Background

Large language models now routinely achieve impressive scores on mathematical contests such as the AIME, IMO, and Putnam. These results suggest substantial progress in mathematical reasoning— however, they come with an important caveat. Natural language solutions can mask subtle logical errors, unstated assumptions, or invalid steps that are difficult and time-consuming for humans to audit.

To address this gap, ProofBench evaluates whether models can translate mathematical reasoning into machine-checkable proofs. We use Lean 4, a proof assistant and programming language designed for formal mathematics, where every logical inference must be formally verified (i.e., be machine-checkable). Since a solution here either compiles or it does not— there is no partial credit for plausible reasoning- this makes for a more objective evaluation of mathematical reasoning skills.

In addition, mathematicians are increasingly using Lean 4 to formalize their work. Therefore, models that perform well on this benchmark will be valuable in assisting with mathematical research in the future.

Success on this benchmark therefore tests whether models can maintain logical correctness across chains of reasoning, and whether they can be effective with modern formal mathematics. Strong performance would indicate genuine progress toward AI systems that can assist mathematicians with formalization, verification, and large-scale proof development.

Results

To visualize the performance differences among language models, we provide scatter plots illustrating accuracy versus latency and cost. These cover the language models only, and not Aristotle, for which neither latency nor cost is recorded.

ProofBench v1.1

Benchmark Overview

Each benchmark task pairs a natural-language mathematical problem with its corresponding Lean 4 formal statement. Given both, a model must construct a formal proof that is accepted by the Lean proof checker. The benchmark measures proof success directly, providing a clear and unforgiving signal of correctness. Problems are drawn from advanced undergraduate and graduate-level sources, including qualifying exams and standard textbooks. They span a broad range of modern mathematics:

Probability theory and stochastic analysis
Measure theory
Real and functional analysis
Algebra and commutative algebra
Algebraic geometry
Number theory
Set theory, logic, and model theory

Tool Use Analysis

Within the ProofBench harness, models have access to tools organized into the following bundles:

Bundle	Tools
Search	lean_loogle (Mathlib search)
Code Execution	lean_run_code (Lean code execution + feedback)
Submission	submit_proof (final proof submission)

Models may iteratively search the Mathlib library and test partial proofs or code in a Lean 4 environment before submitting a final solution. The submission tool is invoked exactly once per problem. The visualization below summarizes how different models allocate effort between search and code execution during problem solving.

Tool Usage Count

8/23 models

Raw call counts across all problemsMost tool calls first

What separates the strongest models here is economy rather than how they split their effort. Claude Opus 5 and Claude Fable 5 are among the strongest models on the board while making far fewer tool calls than most of it — around 14 and 11 per task respectively, where most other models need several times that. They tend to search for a specific lemma, confirm it in Lean, and submit.

The balance between searching and executing code does not by itself predict performance. Models clustered between 59% and 61% code execution score anywhere from 26% to 99%: Claude Opus 5 sits in that band alongside models scoring below 45%. Knowing how a model divides its effort tells you very little about whether it will finish a proof.

What matters more is whether the model commits to an answer at all. A proof is graded only if the model calls submit_proof, and much of the board fails to do so reliably: around half of the models we tested submit on fewer than 95% of problems, exhausting their 40 turns instead. The harness works hard against this, with a turn counter on every turn, escalating warnings from ten turns out, and a final turn where submit_proof is the only tool on offer.

DeepSeek V4 is the extreme case: it submits on 16 problems and proves all 16, yet scores near the bottom because it never submits the other 84. Inkling submits on 28% and scores zero. Both are better described as unable to stop working than unable to do mathematics, and a reader comparing scores at the bottom of this board is largely comparing that, rather than formal-mathematics ability.

A common failure mode is the opposite of economy: models spiralling into long series of search calls after a theorem or notion that does not exist, continuing to try variations rather than changing approach. Gemini 3.1 Pro Preview (02/26) averages 88 tool calls per task and GPT-5.6 Luna 74, both while scoring well below the leaders.

Methodology

The benchmark consists of two splits: a public split and a private test split, each containing 100 problems. For every problem, we provide:

A natural-language statement of the theorem (no informal proof attached; models must generate the proof)
A carefully vetted Lean 4 formalization of the statement

Models are allowed up to 40 interaction turns per problem, enabling iterative development with tool feedback. No access to the informal proof is provided.

Note on evaluating Aristotle: To evaluate Aristotle, a formal-math system from Harmonic AI, we submit the Lean 4 statement file with the proof left as sorry, together with an instruction to complete it that mirrors the system prompt given to every other model — including the requirement that the submission close every goal without sorry, admit, or added axioms. We emphasize that Aristotle uses its own internal system/harness, and not the evaluation harness we provide to other models. Its proofs are checked against the Lean toolchain it works in (4.28), rather than the 4.25.2 toolchain used by the sandbox the other models run in, so that no entrant is penalised for library changes between the two versions; scores are therefore produced against a different Mathlib revision than the rest of the leaderboard. One problem is worth singling out: algebraicGeometry_hartshorne_ch_I_1_ex8, a case of Hartshorne’s result that every irreducible component of the intersection of an affine variety with a hypersurface not containing it drops dimension by exactly one, is a problem that Aristotle proved and no general-purpose model in the v1.1 cohort did. Aristotle’s submission develops roughly 450 lines of supporting Krull-dimension theory — going up and going down for integral extensions, heights of point ideals in polynomial rings, and a version of Krull’s principal ideal theorem for affine domains via Noether normalisation — before proving the statement itself. Aristotle is allowed such auxiliary lemmas because it returns a whole file; the other models submit a proof body and must inline any intermediate results, which is a difference in affordance rather than in mathematics.

Note on what counts as a proof: every accepted submission is checked with #print axioms, and a proof resting on anything the benchmark disallows scores zero — in particular sorry and admit, which surface as sorryAx. native_decide is accepted. It discharges a goal by running compiled code, so it rests on Lean.ofReduceBool and Lean.trustCompiler rather than on the kernel alone, and an earlier revision of the grader rejected it on that basis. We have reversed that: the instructions given to models forbid introducing new axioms, which native_decide does not do, so rejecting it enforced a rule we had not stated. Seven models were affected, on two problems, each by a single task.

Note on cost and latency: both are averaged over all 100 problems, so a problem a model failed to complete still counts against it. For a small number of problems the per-task usage did not reach our results database, and we read it back from the run’s own stored output instead — those figures are measurements from the original run, not a repeat attempt. Three problems produced no output at all: two ended with the model exhausting its 128,000-token limit without emitting a response, and their cost is imputed at that limit priced at the model’s output rate; the third was re-run in the pinned evaluation image. None of this changed any model’s score.

_{Published results are from version 1.1 of the benchmark. Scores are not comparable with results published against earlier revisions.}

Data Collection Process and Examples

Prior benchmarks have faced numerous challenges with ensuring that the formalizations of the statements were correct. Statements may be misformalized in a number of ways, particularly if autoformalized by models. To circumvent these issues, problems were selected and formalized by a team of Lean 4 experts, including PhD students and experts in their respective domains. Statements and formalizations underwent a secondary review process before being included in the benchmark. We also collected natural language proofs for the problems, and while the main scores reported on this page do not give the model(s) access to the proofs, we plan to conduct ablations including the proofs.

For examples of the questions in the benchmark, see the panel below.

Model Output Examples

Question

Show that there exists a bounded continuous $f$ on $(0, +\infty)$ such that $\lim_{x \to +\infty}f(x) \to 0$ but $f \notin L^p (0, \infty)$ for any $p > 0$.

Lean Formalization

1import Mathlib
2
3theorem measure_wheeden_zygmund_ch5_ex12 :
4    ∃ f : ℝ → ℝ, ContinuousOn f (Set.Ioi 0) ∧ (∃ M, ∀ x ∈ Set.Ioi 0, |f x| ≤ M) ∧
5      Filter.Tendsto f Filter.atTop (nhds 0) ∧
6      ∀ p : ℝ, 0 < p →
7        ¬MeasureTheory.MemLp f (ENNReal.ofReal p) (MeasureTheory.volume.restrict (Set.Ioi 0)) :=
8  sorry

Proof

1by
2  have hlog2 : (0:ℝ) < Real.log 2 := Real.log_pos (by norm_num)
3  have helper : ∀ x C A : ℝ, 0 < x → 0 < A → A ≤ C * x → x⁻¹ ≤ C * A⁻¹ := by
4    intro x C A hx hA h
5    have hCx : 0 < A * x := mul_pos hA hx
6    calc x⁻¹ = A / (A * x) := by field_simp
7      _ ≤ (C * x) / (A * x) := by gcongr
8      _ = C * A⁻¹ := by field_simp
9  refine ⟨fun x => (Real.log (x + 2))⁻¹, ?_, ⟨(Real.log 2)⁻¹, ?_⟩, ?_, ?_⟩
10  · have h1 : ContinuousOn (fun x : ℝ => Real.log (x + 2)) (Set.Ioi 0) := by
11      refine ContinuousOn.log (by fun_prop) ?_
12      intro x hx
13      simp only [Set.mem_Ioi] at hx
14      exact ne_of_gt (by linarith)
15    exact h1.inv₀ (fun x hx => (Real.log_pos (by simp only [Set.mem_Ioi] at hx; linarith)).ne')
16  · intro x hx
17    simp only [Set.mem_Ioi] at hx
18    have h3 : Real.log 2 ≤ Real.log (x + 2) := Real.log_le_log (by norm_num) (by linarith)
19    have h4 : (0:ℝ) < Real.log (x + 2) := lt_of_lt_of_le hlog2 h3
20    rw [abs_of_pos (inv_pos.mpr h4)]
21    exact inv_anti₀ hlog2 h3
22  · have h1 : Filter.Tendsto (fun x : ℝ => Real.log (x + 2)) Filter.atTop Filter.atTop :=
23      Real.tendsto_log_atTop.comp (Filter.tendsto_atTop_add_const_right _ 2 Filter.tendsto_id)
24    exact h1.inv_tendsto_atTop
25  · intro p hp hmem
26    have hp0 : ENNReal.ofReal p ≠ 0 := by
27      simp only [ne_eq, ENNReal.ofReal_eq_zero]
28      linarith
29    have hint : MeasureTheory.Integrable
30        (fun x : ℝ => ‖(Real.log (x + 2))⁻¹‖ ^ p) (MeasureTheory.volume.restrict (Set.Ioi 0)) := by
31      have h := hmem.integrable_norm_rpow hp0 ENNReal.ofReal_ne_top
32      rwa [ENNReal.toReal_ofReal hp.le] at h
33    have hint2 : MeasureTheory.IntegrableOn
34        (fun x : ℝ => ‖(Real.log (x + 2))⁻¹‖ ^ p) (Set.Ioi 2) MeasureTheory.volume :=
35      MeasureTheory.IntegrableOn.mono_set hint (Set.Ioi_subset_Ioi (by norm_num))
36    have key : MeasureTheory.IntegrableOn (fun x : ℝ => x ^ (-1:ℝ)) (Set.Ioi 2)
37        MeasureTheory.volume := by
38      refine MeasureTheory.Integrable.mono' (hint2.const_mul ((2*p)^p)) (by fun_prop) ?_
39      filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi] with x hx
40      simp only [Set.mem_Ioi] at hx
41      have hxpos : (0:ℝ) < x := by linarith
42      have hL : (0:ℝ) < Real.log (x + 2) := Real.log_pos (by linarith)
43      have hε : (0:ℝ) < 1 / (2 * p) := by positivity
44      have h1 : Real.log (x + 2) ≤ (x + 2) ^ (1 / (2 * p)) / (1 / (2 * p)) :=
45        Real.log_le_rpow_div (by linarith) hε
46      have h2 : (Real.log (x + 2)) ^ p ≤ ((x + 2) ^ (1 / (2 * p)) / (1 / (2 * p))) ^ p :=
47        Real.rpow_le_rpow hL.le h1 hp.le
48      have h3 : ((x + 2) ^ (1 / (2 * p)) / (1 / (2 * p))) ^ p
49          = (x + 2) ^ ((1:ℝ)/2) * (2 * p) ^ p := by
50        rw [div_eq_mul_inv, Real.mul_rpow (by positivity) (by positivity),
51          ← Real.rpow_mul (by linarith), one_div (2*p), inv_inv]
52        congr 2
53        field_simp
54      have h4 : (x + 2) ^ ((1:ℝ)/2) ≤ x := by
55        rw [← Real.sqrt_eq_rpow]
56        have h : Real.sqrt (x + 2) ≤ Real.sqrt (x^2) := Real.sqrt_le_sqrt (by nlinarith)
57        rwa [Real.sqrt_sq (by linarith)] at h
58      have hA : (Real.log (x + 2)) ^ p ≤ (2 * p) ^ p * x := by
59        calc (Real.log (x + 2)) ^ p ≤ (x + 2) ^ ((1:ℝ)/2) * (2 * p) ^ p := by rw [← h3]; exact h2
60          _ ≤ x * (2 * p) ^ p := mul_le_mul_of_nonneg_right h4 (by positivity)
61          _ = (2 * p) ^ p * x := by ring
62      rw [Real.norm_eq_abs, abs_of_pos (Real.rpow_pos_of_pos hxpos _), Real.rpow_neg_one,
63        Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hL), Real.inv_rpow hL.le]
64      exact helper x ((2*p)^p) ((Real.log (x + 2)) ^ p) hxpos (Real.rpow_pos_of_pos hL p) hA
65    rw [integrableOn_Ioi_rpow_iff (by norm_num : (0:ℝ) < 2)] at key
66    norm_num at key

CORRECT

Verified by Lean.

Question

Show that a Noetherian scheme $X$ is integral if and only if $X$ is nonempty and connected and all stalks $\mathcal{O}_{X, \mathbf{p}}$ are integral domains.

Lean Formalization

1import Mathlib
2
3open AlgebraicGeometry
4
5variable {X : Scheme} [IsNoetherian X]
6
7theorem algebraicGeometry_vakil_ch_5_3_C : IsIntegral X ↔ Nonempty X ∧
8    ConnectedSpace X ∧ ∀ p : X, IsDomain (X.presheaf.stalk p) :=
9  sorry

Proof

1by
2  have genericPointNoProperGeneration : ∀ {Z : Set X}, Z ∈ irreducibleComponents X →
3      ∀ {η : X}, IsGenericPoint η Z → ∀ {w : X}, w ⤳ η → w = η := by
4    intro Z hZ η hη w hw
5    rw [irreducibleComponents_eq_maximals_closed] at hZ
6    have hmax : Maximal (fun s => IsClosed s ∧ IsIrreducible s) Z := hZ
7    have hZsub : Z ⊆ closure {w} := by
8      rw [← hη.def]
9      exact closure_minimal (Set.singleton_subset_iff.mpr (specializes_iff_mem_closure.mp hw)) isClosed_closure
10    have hPclw : IsClosed (closure {w}) ∧ IsIrreducible (closure {w}) :=
11      ⟨isClosed_closure, isIrreducible_singleton.closure⟩
12    have hsub2 : closure {w} ⊆ Z := hmax.le_of_ge hPclw hZsub
13    have heq : closure {w} = Z := le_antisymm hsub2 hZsub
14    have hgw : IsGenericPoint w Z := heq ▸ isGenericPoint_closure
15    exact hgw.eq hη
16  have stalk_not_domain_of_mem_two_components : ∀ {p : X} {Z1 Z2 : Set X},
17      Z1 ∈ irreducibleComponents X → Z2 ∈ irreducibleComponents X → Z1 ≠ Z2 →
18      p ∈ Z1 → p ∈ Z2 → ¬ IsDomain (X.presheaf.stalk p) := by
19    intro p Z1 Z2 hZ1 hZ2 hne hp1 hp2 hdom
20    have hZ1c : IsClosed Z1 ∧ IsIrreducible Z1 := by
21      rw [irreducibleComponents_eq_maximals_closed] at hZ1
22      have : Maximal (fun s => IsClosed s ∧ IsIrreducible s) Z1 := hZ1
23      exact this.prop
24    have hZ2c : IsClosed Z2 ∧ IsIrreducible Z2 := by
25      rw [irreducibleComponents_eq_maximals_closed] at hZ2
26      have : Maximal (fun s => IsClosed s ∧ IsIrreducible s) Z2 := hZ2
27      exact this.prop
28    obtain ⟨η1, hη1⟩ := QuasiSober.sober hZ1c.2 hZ1c.1
29    obtain ⟨η2, hη2⟩ := QuasiSober.sober hZ2c.2 hZ2c.1
30    have hηne : η1 ≠ η2 := by
31      intro he; apply hne; rw [← hη1.def, ← hη2.def, he]
32    have hs1 : η1 ⤳ p := hη1.specializes hp1
33    have hs2 : η2 ⤳ p := hη2.specializes hp2
34    have hmem1 : η1 ∈ Set.range (X.fromSpecStalk p).base := by
35      rw [AlgebraicGeometry.Scheme.range_fromSpecStalk]; exact hs1
36    have hmem2 : η2 ∈ Set.range (X.fromSpecStalk p).base := by
37      rw [AlgebraicGeometry.Scheme.range_fromSpecStalk]; exact hs2
38    obtain ⟨x1, hx1⟩ := hmem1
39    obtain ⟨x2, hx2⟩ := hmem2
40    have hfinj : Function.Injective (X.fromSpecStalk p).base :=
41      (Scheme.Hom.isEmbedding (X.fromSpecStalk p)).injective
42    have hcont : Continuous (X.fromSpecStalk p).base := by fun_prop
43    have hx1ne2 : x1 ≠ x2 := by
44      intro he; apply hηne; rw [← hx1, ← hx2, he]
45    have hgen1 : ∀ w, w ⤳ x1 → w = x1 := by
46      intro w hw
47      have hmap : (X.fromSpecStalk p).base w ⤳ (X.fromSpecStalk p).base x1 := hw.map hcont
48      rw [hx1] at hmap
49      have heq : (X.fromSpecStalk p).base w = η1 := genericPointNoProperGeneration hZ1 hη1 hmap
50      apply hfinj; rw [heq, hx1]
51    have hgen2 : ∀ w, w ⤳ x2 → w = x2 := by
52      intro w hw
53      have hmap : (X.fromSpecStalk p).base w ⤳ (X.fromSpecStalk p).base x2 := hw.map hcont
54      rw [hx2] at hmap
55      have heq : (X.fromSpecStalk p).base w = η2 := genericPointNoProperGeneration hZ2 hη2 hmap
56      apply hfinj; rw [heq, hx2]
57    have hdomain_unique : ∀ {x y : PrimeSpectrum (X.presheaf.stalk p)},
58        (∀ w, w ⤳ x → w = x) → (∀ w, w ⤳ y → w = y) → x = y := by
59      intro x y hx hy
60      set b : PrimeSpectrum (X.presheaf.stalk p) := ⟨⊥, Ideal.bot_prime⟩ with hb
61      have hbx : b ≤ x := by rw [← PrimeSpectrum.asIdeal_le_asIdeal]; exact bot_le
62      have hby : b ≤ y := by rw [← PrimeSpectrum.asIdeal_le_asIdeal]; exact bot_le
63      rw [PrimeSpectrum.le_iff_specializes] at hbx hby
64      have ex : b = x := hx b hbx
65      have ey : b = y := hy b hby
66      rw [← ex, ← ey]
67    exact hx1ne2 (hdomain_unique hgen1 hgen2)
68  constructor
69  · intro hint
70    rw [isIntegral_iff_irreducibleSpace_and_isReduced] at hint
71    obtain ⟨hirr, hred⟩ := hint
72    haveI := hirr
73    refine ⟨hirr.toNonempty, hirr.connectedSpace, ?_⟩
74    intro p
75    have hred_stalk : IsReduced (X.presheaf.stalk p) := isReduced_stalk_of_isReduced X p
76    obtain ⟨η, hη⟩ := QuasiSober.sober (IrreducibleSpace.isIrreducible_univ X) isClosed_univ
77    have hs : η ⤳ p := hη.specializes (Set.mem_univ p)
78    have hmem : η ∈ Set.range (X.fromSpecStalk p).base := by
79      rw [AlgebraicGeometry.Scheme.range_fromSpecStalk]; exact hs
80    obtain ⟨x0, hx0⟩ := hmem
81    have hemb : Topology.IsEmbedding (X.fromSpecStalk p).base := Scheme.Hom.isEmbedding (X.fromSpecStalk p)
82    have hgenall : ∀ y : PrimeSpectrum (X.presheaf.stalk p), x0 ⤳ y := by
83      intro y
84      rw [← hemb.toIsInducing.specializes_iff, hx0]
85      exact hη.specializes (Set.mem_univ _)
86    have hspec_to_le : ∀ (a b : PrimeSpectrum (X.presheaf.stalk p)), a ⤳ b → a.asIdeal ≤ b.asIdeal := by
87      intro a b hab
88      rw [PrimeSpectrum.asIdeal_le_asIdeal, PrimeSpectrum.le_iff_specializes]
89      exact hab
90    have hsub : x0.asIdeal ≤ nilradical (X.presheaf.stalk p) := by
91      rw [nilradical_eq_sInf]
92      refine le_sInf ?_
93      rintro J hJ
94      exact hspec_to_le x0 ⟨J, hJ⟩ (hgenall _)
95    have hbot : x0.asIdeal = ⊥ := by
96      refine le_antisymm ?_ bot_le
97      intro a ha
98      have hnil : IsNilpotent a := mem_nilradical.mp (hsub ha)
99      exact hred_stalk.eq_zero a hnil
100    haveI : (⊥ : Ideal (X.presheaf.stalk p)).IsPrime := hbot ▸ x0.isPrime
101    exact IsDomain.of_bot_isPrime (X.presheaf.stalk p)
102  · rintro ⟨hne, hconn, hdom⟩
103    rw [isIntegral_iff_irreducibleSpace_and_isReduced]
104    haveI : ∀ x : X, IsReduced (X.presheaf.stalk x) := fun x => by
105      have := hdom x; infer_instance
106    have hred : IsReduced X := isReduced_of_isReduced_stalk X
107    refine ⟨?_, hred⟩
108    have hdisj : ∀ Z1 Z2 : Set X, Z1 ∈ irreducibleComponents X → Z2 ∈ irreducibleComponents X →
109        Z1 ≠ Z2 → Disjoint Z1 Z2 := by
110      intro Z1 Z2 hZ1 hZ2 hne'
111      rw [Set.disjoint_left]
112      intro p hp1 hp2
113      exact (stalk_not_domain_of_mem_two_components hZ1 hZ2 hne' hp1 hp2) (hdom p)
114    obtain ⟨p0⟩ := hne
115    set Z0 := irreducibleComponent p0 with hZ0def
116    have hZ0mem : Z0 ∈ irreducibleComponents X := irreducibleComponent_mem_irreducibleComponents p0
117    have hZ0irr : IsIrreducible Z0 := isIrreducible_irreducibleComponent
118    have hZ0closed : IsClosed Z0 := isClosed_irreducibleComponent
119    have hfin : (irreducibleComponents X).Finite := TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
120    have hcompl : Z0ᶜ = ⋃ Z ∈ (irreducibleComponents X \ {Z0}), Z := by
121      ext x
122      simp only [Set.mem_compl_iff, Set.mem_iUnion, Set.mem_diff, Set.mem_singleton_iff]
123      constructor
124      · intro hx
125        refine ⟨irreducibleComponent x, ⟨irreducibleComponent_mem_irreducibleComponents x, ?_⟩, mem_irreducibleComponent⟩
126        intro he
127        exact hx (he ▸ mem_irreducibleComponent)
128      · rintro ⟨Z, ⟨hZmem, hZne⟩, hxZ⟩ hx0
129        exact absurd hx0 (Set.disjoint_left.mp (hdisj Z Z0 hZmem hZ0mem hZne) hxZ)
130    have hclosed_compl : IsClosed Z0ᶜ := by
131      rw [hcompl]
132      exact Set.Finite.isClosed_biUnion (hfin.subset Set.diff_subset)
133        (fun Z hZ => isClosed_of_mem_irreducibleComponents Z hZ.1)
134    have hZ0open : IsOpen Z0 := by
135      rw [← compl_compl Z0]
136      exact isOpen_compl_iff.mpr hclosed_compl
137    have hZ0clopen : IsClopen Z0 := ⟨hZ0closed, hZ0open⟩
138    rcases isClopen_iff.mp hZ0clopen with h0 | h0
139    · exact absurd h0 hZ0irr.nonempty.ne_empty
140    · have hirrunivZ : IsIrreducible (Set.univ : Set X) := h0 ▸ hZ0irr
141      exact irreducibleSpace_def X |>.mpr (by simpa using hirrunivZ)

CORRECT

Verified by Lean.

Acknowledgements

We thank Kexing Ying, Vasilii Nesterov, Janitha Aswedige, Bingyu Xia, Elif Uskuplu, and Yizheng Zhu for contributing problem formalizations. We also thank Alex Gu for valuable feedback that improved the benchmark design. Finally, we are grateful to the teams behind lean-lsp-mcp, as well as Loogle.

Citations

If you use this benchmark in your research, please cite the paper.

[1] Formal Mathematical Reasoning: A New Frontier in AI (arXiv:2412.16075)
[2] The Lean 4 language (lean-lang.org)

Citation (BibTeX)

@inproceedings{ravi2026formalproofbench,
title        = {FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?},
author       = {Nikil Ravi and Kexing Ying and Vasilii Nesterov and Rayan Krishnan and Elif Uskuplu and Bingyu Xia and Janitha Aswedige and Langston Nashold},
booktitle    = {ICLR 2026 Workshop: VerifAI-2: The Second Workshop on AI Verification in the Wild},
year         = {2026},
url          = {https://arxiv.org/abs/2603.26996},
}