How far are prover proofs from the fewest steps?
The 256 DeepSeek-Prover miniF2F proofs that compile in Lean 4.24 shrink from 9640 to 3076 tactic steps (68% fewer). 70% of the results carry a certificate that no shorter proof exists over the searched tactic list.
Data: 439 DeepSeek-Prover-V1.5 proofs of miniF2F test and valid problems (dataset LukeBailey181/minif2f_proofnet_deepseek_prover_sols). 256 compile unchanged in Lean 4.24 + Mathlib; the rest broke on Mathlib renames since Lean 4.9 and are excluded. Every output was re-checked in a separate pass under its original name, one file per proof. 22 of 512 failed that check; for those the original proof is kept and counted with no cut.
Results
| Minimal mode | Clear mode | |
|---|---|---|
| Proofs that compile in Lean 4.24 | 256 | 256 |
| Total steps before | 9640 | 9640 |
| Total steps after | 3076 | 4674 |
| Steps cut, all proofs | 68% | 52% |
| Steps cut, proofs of 20+ steps | 66% | 49% |
| Median steps before → after | 25.0 → 1.0 | 25.0 → 2.0 |
| Proofs that became one tactic | 61% | 45% |
| Certified optimal | 70% | 54% |
| Characters cut | 64% | 49% |
Clear mode bans aesop, grind, decide, tauto and simp_all, so every step is one a reader can redo by hand.
Gap between found proof and lower bound (minimal)
| Steps above the bound | Proofs |
|---|---|
| 0 (optimal) | 180 |
| 1 to 5 | 11 |
| 6 to 20 | 28 |
| 21 to 100 | 21 |
| over 100 | 6 |
| no bound | 10 |
Method
A step is one tactic invocation; have h : x := by ring counts 2, a <;> b counts 2. The tactic list for each theorem is 16 generic tactics plus every one-line tactic the original proof uses, with its arguments.
Lower bound: Euled compiles every 1-step proof from the list, and every 2-step proof (sequenced and with <;>) when the list has at most 31 entries. If none compiles, no proof of that length exists over the list.
Upper bound: from the original proof, Euled repeatedly tries deleting any one statement and replacing the tail of any tactic block, from any position, with one tactic from the list. It keeps the shortest proof Lean accepts and stops when a full pass gains nothing. A proof is certified optimal when its length equals the lower bound.
All checks ran on AXLE with no language model. Median time per proof: 25.950000000000003 s.
Largest cuts
mathd_numbertheory_483: 145 → 1 steps
DeepSeek-Prover proof
theorem mathd_numbertheory_483 (a : ℕ → ℕ) (h₀ : a 1 = 1) (h₁ : a 2 = 1)
(h₂ : ∀ n, a (n + 2) = a (n + 1) + a n) : a 100 % 4 = 3 := by
have h₃ : a 0 = 0 := by
have h₄ := h₂ 0
simp [h₀, h₁] at h₄
<;> omega
have h₄ : a 3 = 2 := by
have h₅ := h₂ 1
have h₆ := h₂ 2
have h₇ := h₂ 3
simp [h₀, h₁, h₃] at h₅ h₆ h₇
<;> omega
have h₅ : a 4 = 3 := by
have h₅ := h₂ 2
have h₆ := h₂ 3
have h₇ := h₂ 4
simp [h₀, h₁, h₃, h₄] at h₅ h₆ h₇
<;> omega
have h₆ : a 5 = 5 := by
have h₆ := h₂ 3
have h₇ := h₂ 4
have h₈ := h₂ 5
simp [h₀, h₁, h₃, h₄, h₅] at h₆ h₇ h₈
<;> omega
have h₇ : a 6 = 8 := by
have h₇ := h₂ 4
have h₈ := h₂ 5
have h₉ := h₂ 6
simp [h₀, h₁, h₃, h₄, h₅, h₆] at h₇ h₈ h₉
<;> omega
have h₈ : a 7 = 13 := by
have h₈ := h₂ 5
have h₉ := h₂ 6
have h₁₀ := h₂ 7
simp [h₀, h₁, h₃, h₄, h₅, h₆, h₇] at h₈ h₉ h₁₀
<;> omega
have h₉ : a 8 = 21 := by
have h₉ := h₂ 6
have h₁₀ := h₂ 7
have h₁₁ := h₂ 8
simp [h₀, h₁, h₃, h₄, h₅, h₆, h₇, h₈] at h₉ h₁₀ h₁₁
<;> omega
have h₁₀ : a 9 = 34 := by
have h₁₀ := h₂ 7
have h₁₁ := h₂ 8
have h₁₂ := h₂ 9
simp [h₀, h₁, h₃, h₄, h₅, h₆, h₇, h₈, h₉] at h₁₀ h₁₁ h₁₂
<;> omega
have h₁₁ : a 10 = 55 := by
have h₁₁ := h₂ 8
have h₁₂ := h₂ 9
have h₁₃ := h₂ 10
simp [h₀, h₁, h₃, h₄, h₅, h₆, h₇, h₈, h₉, h₁₀] at h₁₁ h₁₂ h₁₃
<;> omega
have h₁₂ : ∀ n, a (n + 6) % 4 = a n % 4 := by
intro n
have h₁₃ : a (n + 6) = 8 * a (n + 1) + 5 * a n := by
have h₁₄ := h₂ n
have h₁₅ := h₂ (n + 1)
have h₁₆ := h₂ (n + 2)
have h₁₇ := h₂ (n + 3)
have h₁₈ := h₂ (n + 4)
have h₁₉ := h₂ (n + 5)
have h₂₀ := h₂ (n + 6)
have h₂₁ := h₂ (n + 7)
have h₂₂ := h₂ (n + 8)
have h₂₃ := h₂ (n + 9)
simp [add_assoc, add_comm, add_left_comm] at h₁₄ h₁₅ h₁₆ h₁₇ h₁₈ h₁₉ h₂₀ h₂₁ h₂₂ h₂₃ ⊢
ring_nf at h₁₄ h₁₅ h₁₆ h₁₇ h₁₈ h₁₉ h₂₀ h₂₁ h₂₂ h₂₃ ⊢
<;>
(try omega) <;>
(try nlinarith) <;>
(try ring_nf at h₁₄ h₁₅ h₁₆ h₁₇ h₁₈ h₁₉ h₂₀ h₂₁ h₂₂ h₂₃ ⊢ <;> omega) <;>
(try nlinarith) <;>
(try omega) <;>
(try nlinarith) <;>
(try omega)
rw [h₁₃]
have h₂₄ : (8 * a (n + 1) + 5 * a n) % 4 = a n % 4 := by
have h₂₅ : (8 * a (n + 1) + 5 * a n) % 4 = (a n % 4) := by
have h₂₆ : a (n + 1) % 4 = a (n + 1) % 4 := rfl
have h₂₇ : a n % 4 = a n % 4 := rfl
have h₂₈ : (8 * a (n + 1) + 5 * a n) % 4 = (a n % 4) := by
have h₂₉ : (8 * a (n + 1) + 5 * a n) % 4 = ((8 * a (n + 1)) % 4 + (5 * a n) % 4) % 4 := by
omega
rw [h₂₉]
have h₃₀ : (8 * a (n + 1)) % 4 = 0 := by
have h₃₁ : (8 * a (n + 1)) % 4 = 0 := by
omega
exact h₃₁
have h₃₂ : (5 * a n) % 4 = (a n) % 4 := by
have h₃₃ : (5 * a n) % 4 = (a n) % 4 := by
omega
exact h₃₃
omega
exact h₂₈
omega
omega
have h₁₃ : a 100 % 4 = 3 := by
have h₁₄ : a 100 % 4 = 3 := by
have h₁₅ : a 100 % 4 = a 4 % 4 := by
have h₁₆ : a 100 % 4 = a 4 % 4 := by
have h₁₇ : a 100 % 4 = a 4 % 4 := by
have h₁₈ : a 100 % 4 = a 4 % 4 := by
have h₁₉ := h₁₂ 94
have h₂₀ := h₁₂ 88
have h₂₁ := h₁₂ 82
have h₂₂ := h₁₂ 76
have h₂₃ := h₁₂ 70
have h₂₄ := h₁₂ 64
have h₂₅ := h₁₂ 58
have h₂₆ := h₁₂ 52
have h₂₇ := h₁₂ 46
have h₂₈ := h₁₂ 40
have h₂₉ := h₁₂ 34
have h₃₀ := h₁₂ 28
have h₃₁ := h₁₂ 22
have h₃₂ := h₁₂ 16
have h₃₃ := h₁₂ 10
have h₃₄ := h₁₂ 4
norm_num at h₁₉ h₂₀ h₂₁ h₂₂ h₂₃ h₂₄ h₂₅ h₂₆ h₂₇ h₂₈ h₂₉ h₃₀ h₃₁ h₃₂ h₃₃ h₃₄ ⊢
<;>
(try omega) <;>
(try ring_nf at h₁₉ h₂₀ h₂₁ h₂₂ h₂₃ h₂₄ h₂₅ h₂₆ h₂₇ h₂₈ h₂₉ h₃₀ h₃₁ h₃₂ h₃₃ h₃₄ ⊢) <;>
(try omega) <;>
(try ring_nf) <;>
(try omega)
exact h₁₈
exact h₁₇
exact h₁₆
have h₁₅₁ : a 4 % 4 = 3 := by
norm_num [h₅]
rw [h₁₅]
exact h₁₅₁
exact h₁₄
exact h₁₃
theorem mathd_numbertheory_483 (a : ℕ → ℕ) (h₀ : a 1 = 1) (h₁ : a 2 = 1)
(h₂ : ∀ n, a (n + 2) = a (n + 1) + a n) : a 100 % 4 = 3 := by
aesop
aime_1997_p9: 165 → 29 steps
DeepSeek-Prover proof
theorem aime_1997_p9 (a : ℝ) (h₀ : 0 < a)
(h₁ : 1 / a - Int.floor (1 / a) = a ^ 2 - Int.floor (a ^ 2)) (h₂ : 2 < a ^ 2) (h₃ : a ^ 2 < 3) :
a ^ 12 - 144 * (1 / a) = 233 := by
have h₄ : Int.floor (a ^ 2 : ℝ) = 2 := by
rw [Int.floor_eq_iff]
constructor <;> norm_num at h₂ h₃ ⊢ <;>
(try norm_num) <;>
(try nlinarith) <;>
(try linarith) <;>
(try nlinarith [h₀, h₂, h₃])
<;>
(try norm_num at h₂ h₃ ⊢) <;>
(try nlinarith) <;>
(try linarith) <;>
(try nlinarith [h₀, h₂, h₃])
<;>
(try norm_num at h₂ h₃ ⊢) <;>
(try nlinarith) <;>
(try linarith) <;>
(try nlinarith [h₀, h₂, h₃])
have h₅ : Int.floor (1 / a : ℝ) = 0 := by
have h₅₁ : 0 < (1 / a : ℝ) := by positivity
have h₅₂ : (1 / a : ℝ) < 1 := by
have h₅₂₁ : 0 < a := h₀
have h₅₂₂ : 0 < a ^ 2 := by positivity
have h₅₂₃ : a ^ 2 < 3 := h₃
have h₅₂₄ : 2 < a ^ 2 := h₂
have h₅₂₅ : a > 1 := by
by_contra h
have h₅₂₆ : a ≤ 1 := by linarith
have h₅₂₇ : a ^ 2 ≤ 1 := by
nlinarith
linarith
have h₅₂₈ : (1 / a : ℝ) < 1 := by
rw [div_lt_one (by positivity)]
<;> nlinarith
exact h₅₂₈
have h₅₃ : Int.floor (1 / a : ℝ) = 0 := by
rw [Int.floor_eq_iff]
norm_num at h₅₂ ⊢
constructor <;> nlinarith
exact h₅₃
have h₆ : 1 / a = a ^ 2 - 2 := by
have h₆₁ : (1 / a : ℝ) - ⌊(1 / a : ℝ)⌋ = a ^ 2 - ⌊(a ^ 2 : ℝ)⌋ := by simpa using h₁
rw [h₅, h₄] at h₆₁
ring_nf at h₆₁ ⊢
<;> linarith
have h₇ : a ^ 3 - 2 * a - 1 = 0 := by
have h₇₁ : a ≠ 0 := by positivity
have h₇₂ : 1 / a = a ^ 2 - 2 := h₆
have h₇₃ : a ^ 3 - 2 * a - 1 = 0 := by
have h₇₄ : a ^ 3 - 2 * a - 1 = 0 := by
have h₇₅ : 1 / a = a ^ 2 - 2 := h₆
have h₇₆ : a ≠ 0 := by positivity
field_simp at h₇₅
ring_nf at h₇₅ ⊢
nlinarith [sq_nonneg (a - 1), sq_nonneg (a + 1), sq_nonneg (a ^ 2 - 1)]
exact h₇₄
exact h₇₃
have h₈ : a ^ 2 - a - 1 = 0 := by
have h₈₁ : a ≠ 0 := by positivity
have h₈₂ : a ^ 3 - 2 * a - 1 = 0 := h₇
have h₈₃ : a ^ 2 - a - 1 = 0 := by
have h₈₄ : a ^ 3 - 2 * a - 1 = 0 := h₇
have h₈₅ : (a + 1) * (a ^ 2 - a - 1) = 0 := by
ring_nf at h₈₄ ⊢
nlinarith [sq_nonneg (a - 1), sq_nonneg (a + 1), sq_nonneg (a ^ 2 - 1)]
have h₈₆ : a + 1 > 0 := by nlinarith
have h₈₇ : a ^ 2 - a - 1 = 0 := by
apply mul_left_cancel₀ (show (a + 1 : ℝ) ≠ 0 by nlinarith)
nlinarith
exact h₈₇
exact h₈₃
have h₉ : a ^ 12 - 144 * (1 / a) = 233 := by
have h₉₁ : a ^ 2 = a + 1 := by
have h₉₁₁ : a ^ 2 - a - 1 = 0 := h₈
nlinarith
have h₉₂ : a ^ 3 = 2 * a + 1 := by
have h₉₂₁ : a ^ 3 - 2 * a - 1 = 0 := h₇
nlinarith
have h₉₃ : a ^ 4 = 3 * a + 2 := by
calc
a ^ 4 = a * a ^ 3 := by ring
_ = a * (2 * a + 1) := by rw [h₉₂]
_ = 2 * a ^ 2 + a := by ring
_ = 2 * (a + 1) + a := by rw [h₉₁]
_ = 3 * a + 2 := by ring
have h₉₄ : a ^ 5 = 5 * a + 3 := by
calc
a ^ 5 = a * a ^ 4 := by ring
_ = a * (3 * a + 2) := by rw [h₉₃]
_ = 3 * a ^ 2 + 2 * a := by ring
_ = 3 * (a + 1) + 2 * a := by rw [h₉₁]
_ = 5 * a + 3 := by ring
have h₉₅ : a ^ 6 = 8 * a + 5 := by
calc
a ^ 6 = a * a ^ 5 := by ring
_ = a * (5 * a + 3) := by rw [h₉₄]
_ = 5 * a ^ 2 + 3 * a := by ring
_ = 5 * (a + 1) + 3 * a := by rw [h₉₁]
_ = 8 * a + 5 := by ring
have h₉₆ : a ^ 12 = 233 + 144 * (1 / a) := by
calc
a ^ 12 = (a ^ 6) ^ 2 := by ring
_ = (8 * a + 5) ^ 2 := by rw [h₉₅]
_ = 64 * a ^ 2 + 80 * a + 25 := by ring
_ = 64 * (a + 1) + 80 * a + 25 := by rw [h₉₁]
_ = 144 * a + 89 := by ring
_ = 233 + 144 * (1 / a) := by
have h₉₆₁ : 1 / a = a ^ 2 - 2 := h₆
have h₉₆₂ : a ^ 2 = a + 1 := h₉₁
have h₉₆₃ : 1 / a = (a + 1 : ℝ) - 2 := by
rw [h₉₆₁, h₉₆₂]
<;> ring_nf
have h₉₆₄ : (a : ℝ) ≠ 0 := by positivity
field_simp [h₉₆₄] at h₉₆₁ h₉₆₃ ⊢
nlinarith
_ = 233 + 144 * (1 / a) := by ring
have h₉₇ : a ^ 12 - 144 * (1 / a) = 233 := by
calc
a ^ 12 - 144 * (1 / a) = (233 + 144 * (1 / a)) - 144 * (1 / a) := by rw [h₉₆]
_ = 233 := by ring
exact h₉₇
apply h₉
theorem aime_1997_p9 (a : ℝ) (h₀ : 0 < a)
(h₁ : 1 / a - Int.floor (1 / a) = a ^ 2 - Int.floor (a ^ 2)) (h₂ : 2 < a ^ 2) (h₃ : a ^ 2 < 3) :
a ^ 12 - 144 * (1 / a) = 233 := by
have h₄ : Int.floor (a ^ 2 : ℝ) = 2 := by
rw [Int.floor_eq_iff]
grind
have h₅ : Int.floor (1 / a : ℝ) = 0 := by
have h₅₁ : 0 < (1 / a : ℝ) := by positivity
have h₅₂ : (1 / a : ℝ) < 1 := by
have h₅₂₁ : 0 < a := h₀
have h₅₂₂ : 0 < a ^ 2 := by positivity
have h₅₂₃ : a ^ 2 < 3 := h₃
have h₅₂₄ : 2 < a ^ 2 := h₂
have h₅₂₈ : (1 / a : ℝ) < 1 := by
rw [div_lt_one (by positivity)]
<;> nlinarith
exact h₅₂₈
have h₅₃ : Int.floor (1 / a : ℝ) = 0 := by
rw [Int.floor_eq_iff]
norm_num at h₅₂ ⊢
constructor <;> nlinarith
exact h₅₃
have h₆ : 1 / a = a ^ 2 - 2 := by
have h₆₁ : (1 / a : ℝ) - ⌊(1 / a : ℝ)⌋ = a ^ 2 - ⌊(a ^ 2 : ℝ)⌋ := by simpa using h₁
rw [h₅, h₄] at h₆₁
ring_nf at h₆₁ ⊢
<;> linarith
grind
mathd_algebra_452: 121 → 1 steps
DeepSeek-Prover proof
theorem mathd_algebra_452 (a : ℕ → ℝ) (h₀ : ∀ n, a (n + 2) - a (n + 1) = a (n + 1) - a n)
(h₁ : a 1 = 2 / 3) (h₂ : a 9 = 4 / 5) : a 5 = 11 / 15 := by
have h₃ : a 2 - a 1 = a 1 - a 0 := by
have h₃₁ := h₀ 0
norm_num at h₃₁ ⊢
<;> linarith
have h₄ : a 3 - a 2 = a 1 - a 0 := by
have h₄₁ := h₀ 1
have h₄₂ := h₀ 0
have h₄₃ : a 3 - a 2 = a 2 - a 1 := by
linarith
linarith
have h₅ : a 4 - a 3 = a 1 - a 0 := by
have h₅₁ := h₀ 2
have h₅₂ := h₀ 1
have h₅₃ := h₀ 0
have h₅₄ : a 4 - a 3 = a 3 - a 2 := by linarith
linarith
have h₆ : a 5 - a 4 = a 1 - a 0 := by
have h₆₁ := h₀ 3
have h₆₂ := h₀ 2
have h₆₃ := h₀ 1
have h₆₄ := h₀ 0
have h₆₅ : a 5 - a 4 = a 4 - a 3 := by linarith
linarith
have h₇ : a 6 - a 5 = a 1 - a 0 := by
have h₇₁ := h₀ 4
have h₇₂ := h₀ 3
have h₇₃ := h₀ 2
have h₇₄ := h₀ 1
have h₇₅ := h₀ 0
have h₇₆ : a 6 - a 5 = a 5 - a 4 := by linarith
linarith
have h₈ : a 7 - a 6 = a 1 - a 0 := by
have h₈₁ := h₀ 5
have h₈₂ := h₀ 4
have h₈₃ := h₀ 3
have h₈₄ := h₀ 2
have h₈₅ := h₀ 1
have h₈₆ := h₀ 0
have h₈₇ : a 7 - a 6 = a 6 - a 5 := by linarith
linarith
have h₉ : a 8 - a 7 = a 1 - a 0 := by
have h₉₁ := h₀ 6
have h₉₂ := h₀ 5
have h₉₃ := h₀ 4
have h₉₄ := h₀ 3
have h₉₅ := h₀ 2
have h₉₆ := h₀ 1
have h₉₇ := h₀ 0
have h₉₈ : a 8 - a 7 = a 7 - a 6 := by linarith
linarith
have h₁₀ : a 9 - a 8 = a 1 - a 0 := by
have h₁₀₁ := h₀ 7
have h₁₀₂ := h₀ 6
have h₁₀₃ := h₀ 5
have h₁₀₄ := h₀ 4
have h₁₀₅ := h₀ 3
have h₁₀₆ := h₀ 2
have h₁₀₇ := h₀ 1
have h₁₀₈ := h₀ 0
have h₁₀₉ : a 9 - a 8 = a 8 - a 7 := by linarith
linarith
have h₁₁ : a 9 - a 1 = 8 * (a 1 - a 0) := by
have h₁₁₁ : a 9 - a 1 = (a 9 - a 8) + (a 8 - a 7) + (a 7 - a 6) + (a 6 - a 5) + (a 5 - a 4) + (a 4 - a 3) + (a 3 - a 2) + (a 2 - a 1) := by
linarith
rw [h₁₁₁]
have h₁₁₂ : a 9 - a 8 = a 1 - a 0 := by linarith
have h₁₁₃ : a 8 - a 7 = a 1 - a 0 := by linarith
have h₁₁₄ : a 7 - a 6 = a 1 - a 0 := by linarith
have h₁₁₅ : a 6 - a 5 = a 1 - a 0 := by linarith
have h₁₁₆ : a 5 - a 4 = a 1 - a 0 := by linarith
have h₁₁₇ : a 4 - a 3 = a 1 - a 0 := by linarith
have h₁₁₈ : a 3 - a 2 = a 1 - a 0 := by linarith
have h₁₁₉ : a 2 - a 1 = a 1 - a 0 := by linarith
linarith
have h₁₂ : a 1 - a 0 = 1 / 60 := by
have h₁₂₁ : a 9 - a 1 = 8 * (a 1 - a 0) := h₁₁
have h₁₂₂ : a 9 - a 1 = 2 / 15 := by
rw [h₂, h₁]
<;> norm_num
have h₁₂₃ : 8 * (a 1 - a 0) = 2 / 15 := by linarith
have h₁₂₄ : a 1 - a 0 = 1 / 60 := by
ring_nf at h₁₂₃ ⊢
linarith
exact h₁₂₄
have h₁₃ : a 5 - a 1 = 4 * (a 1 - a 0) := by
have h₁₃₁ : a 5 - a 1 = (a 5 - a 4) + (a 4 - a 3) + (a 3 - a 2) + (a 2 - a 1) := by
ring
rw [h₁₃₁]
have h₁₃₂ : a 5 - a 4 = a 1 - a 0 := h₆
have h₁₃₃ : a 4 - a 3 = a 1 - a 0 := h₅
have h₁₃₄ : a 3 - a 2 = a 1 - a 0 := h₄
have h₁₃₅ : a 2 - a 1 = a 1 - a 0 := h₃
linarith
have h₁₄ : a 5 - a 1 = 1 / 15 := by
rw [h₁₃, h₁₂]
<;> ring_nf
<;> norm_num
have h₁₅ : a 5 = 11 / 15 := by
have h₁₅₁ : a 5 = 11 / 15 := by
have h₁₅₂ : a 5 - a 1 = 1 / 15 := h₁₄
have h₁₅₃ : a 1 = 2 / 3 := h₁
have h₁₅₄ : a 5 = 11 / 15 := by
linarith
exact h₁₅₄
exact h₁₅₁
apply h₁₅
theorem mathd_algebra_452 (a : ℕ → ℝ) (h₀ : ∀ n, a (n + 2) - a (n + 1) = a (n + 1) - a n)
(h₁ : a 1 = 2 / 3) (h₂ : a 9 = 4 / 5) : a 5 = 11 / 15 := by
grind
Limits
The bound covers only the searched tactic list. A tactic with different arguments, such as nlinarith [sq_nonneg (a + b)] when the original never used that hint, could give a shorter proof. Many miniF2F problems are easy, so a single strong tactic often closes them; the large step cut says more about prover verbosity than about hard mathematics. Proofs that failed to compile in Lean 4.24 are excluded, which may bias the sample toward simpler proofs.
Raw data: minimal, clear. Code: stepopt.py.