Failure taxonomy

How proofs fail

Every failed attempt is classified by its first Lean error, using only Lean's own message. Unknown names are split into hallucinated and wrong-namespace by looking the name up in the full table of 473,141 constants from the pinned Mathlib.

Counts by configuration

Error classDirectDirect ×4Direct (paraphrased prompt)Full (plan + retrieval + repair)Full − compiler feedbackFull − memoryFull − retrievalFull − skeletonHybrid retrievalHybrid retrieval + repairBM25 retrieval + repairDense retrieval + repairRepairRepair (paraphrased prompt)Template (no LLM)
Wrong tactic39 23%155 22%49 29%34 5%40 6%35 5%34 5%118 18%58 34%144 21%146 22%137 20%103 16%106 16%1710 72%
Syntax error56 32%221 32%46 27%95 15%101 15%88 13%92 14%128 20%47 27%152 23%152 23%159 24%175 26%163 25%0 0%
Lean 3 syntax37 21%146 21%27 16%102 16%97 15%104 16%110 17%118 18%27 16%84 13%96 15%100 15%106 16%78 12%0 0%
Hallucinated theorem23 13%87 13%34 20%48 7%58 9%46 7%69 10%56 9%11 6%69 10%74 11%59 9%137 21%177 27%0 0%
Forbidden token0 0%1 0%2 1%222 34%187 28%226 34%208 31%13 2%1 1%13 2%17 3%9 1%17 3%15 2%0 0%
Other3 2%11 2%2 1%48 7%41 6%43 7%29 4%34 5%9 5%55 8%40 6%53 8%21 3%26 4%411 17%
Type mismatch5 3%15 2%2 1%41 6%45 7%45 7%42 6%56 9%7 4%59 9%34 5%60 9%28 4%27 4%4 0%
Incorrect rewrite3 2%24 3%3 2%38 6%47 7%41 6%31 5%55 8%6 4%36 5%48 7%42 6%22 3%17 3%0 0%
Valid but mathematically wrong3 2%5 1%0 0%6 1%10 2%6 1%4 1%7 1%1 1%8 1%10 2%12 2%12 2%2 0%233 10%
Wrong namespace4 2%24 3%4 2%19 3%26 4%19 3%30 5%27 4%2 1%22 3%23 3%15 2%35 5%36 5%0 0%
Instance resolution failure0 0%0 0%0 0%0 0%0 0%2 0%5 1%37 6%2 1%21 3%15 2%23 3%3 0%3 0%10 0%
Unresolved metavariable0 0%0 0%0 0%0 0%1 0%1 0%7 1%0 0%0 0%2 0%0 0%1 0%0 0%5 1%0 0%
Bad induction0 0%0 0%0 0%0 0%3 0%0 0%0 0%2 0%0 0%0 0%0 0%0 0%5 1%3 0%0 0%
Rejected by certifier0 0%0 0%0 0%1 0%4 1%1 0%0 0%0 0%0 0%3 0%0 0%1 0%0 0%0 0%0 0%
Timeout0 0%0 0%0 0%0 0%0 0%0 0%0 0%0 0%0 0%4 1%3 0%0 0%0 0%0 0%1 0%

Definitions and examples

Hallucinated theorem
Lean reports an unknown name, and no constant with that name exists in the pinned Mathlib under any namespace or capitalisation.
Example proof (mh_cate_15119d, Direct)
rw [Nat.card_eq, CategoryTheory.nat_trans_obj_map_eq, CategoryTheory.isomorphic_map]
Lean output
4:19: error: Unknown identifier `CategoryTheory.nat_trans_obj_map_eq`
3:186: error: unsolved goals
C : Type u₁
inst✝ : CategoryTheory.Category.{u₂, u₁} C
F : CategoryTheory.Functor C FintypeCat
X Y : C
i : X ≅ Y
⊢ (if x : Finite (F.obj X).obj then Fintype.card (F.obj X).obj else 0) = Nat.card (F.obj Y).obj
Wrong namespace
Unknown name, but a constant with the same name exists under another namespace or capitalisation — often a Lean 3 name such as `real.sqrt` for `Real.sqrt`.
Example proof (mh_ineq_f31eb9, Direct)
constructor
intro x
apply le_Inf
intro h
use 0
exact le_zero (le_of_neg_le_zero h)
Lean output
6:8: error: Unknown identifier `le_Inf`
7:8: error: No goals to be solved
Lean 3 syntax
A parse error in a proof written with Lean 3 constructs (`begin … end`, `assume`, `λ x, …`, `cases h with …`).
Example proof (mh_cate_a78895, Direct)
apply_instance
obtain {subobject_classifier} := CategoryTheory.EssentiallySmall.hasSubobjectClassifier_of_essentially_small C
apply (CategoryTheory.Functor.map_subobject_classifier subobject_classifier)
Lean output
4:3: error: unknown tactic
3:193: error: unsolved goals
C : Type u
inst✝¹ : CategoryTheory.Category.{v, u} C
inst✝ : CategoryTheory.EssentiallySmall.{w, v, u} C
⊢ CategoryTheory.HasSubobjectClassifier (CategoryTheory.Functor Cᵒᵖ (Type w))
Syntax error
Any other parse error.
Example proof (mh_cate_431372, Direct)
apply CategoryTheory.Limits.hasColimitsOfShape_of_hasBinaryProducts_of_hasInitialObject;
  · apply FintypeCat.hasBinaryProducts
  · apply FintypeCat.hasInitialObject
Lean output
4:8: error: Unknown identifier `CategoryTheory.Limits.hasColimitsOfShape_of_hasBinaryProducts_of_hasInitialObject`
5:4: error: No goals to be solved
6:4: error: unexpected token '·'; expected command
Type mismatch
A term's type differs from the one expected.
Example proof (mh_func_e6d870, Direct)
intro h; exact h
Lean output
4:11: error: Type mismatch
  h
has type
  Bool
of sort `Type` but is expected to have type
  (!!h) = h
of sort `Prop`
Unresolved metavariable
Lean cannot fill a placeholder or implicit argument.
Example proof (mh_cate_cd9a3b, Full − compiler feedback)
have h_multiplicative := CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre
have h_two_out_of_three := CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsoModSerre
have h_stable_under_retracts := CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre
have h_contains_isomorphisms := CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre
exact CategoryTheory.Morphi
Lean output
4:27: error: typeclass instance problem is stuck
  CategoryTheory.Abelian ?m.14

Note: Lean will not try to resolve this typeclass instance problem because the first and second type arguments to `CategoryTheory.Abelian` are metavariables. These arguments must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functi
Instance resolution failure
Type-class synthesis failed (`failed to synthesize …`).
Example proof (mh_sets_42f697, Full − memory)
constructor
· intro h_mono
  intro s
  intro a
  intro ha
  have : a ∉ s := ha
  rw [Finset.cons_eq_insert]
  exact h_mono _ _ (Finset.insert_subset.2 ha) (Finset.insert_subset.1 (by assumption))
· intro h_add
  intro a b
  intro hab
  have : b ∈ Finset.singleton b := by constructor
  have : b ∉ Finset.singleton b := by constructor
  let s := Finset.singleton b
  have : a ∉ s := by rfl
  exact h_a
Lean output
10:8: error: failed to synthesize instance of type class
  DecidableEq α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
11:10: error: Function expected at
  h_mono ?m.37
but this term has type
  f ?m.35 ≤ f ?m.36

Note: Expected a function because this term is being applied to the argument
  _
5:2: error: unsolved goals
Incorrect rewrite
`rw` found no instance of the pattern, or the motive was not type-correct.
Example proof (mh_sets_64ee0a, Direct)
rw [lt_iff_le_and_ne]
constructor
· exact (le_card_subset_right h).trans (le_trans (le_card_subset_left h) (le_refl _))
· rintro rfl
  exact h.not_le rfl
Lean output
4:6: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?m.10 < ?m.11
in the target expression
  s.card ⋖ t.card

α : Type u_1
s t : Finset α
h : s ⋖ t
⊢ s.card ⋖ t.card
Bad induction
Invalid or missing induction/cases alternatives, or induction on a non-inductive target.
Example proof (novel_set_02, Full − compiler feedback)
have h1 : A ∪ B ⊆ B := by
  intro x
  cases x
  exact h
have h2 : B ⊆ A ∪ B := by
  intro x
  exact Or.inl x
exact Set.Subset.antisymm h1 h2
Lean output
6:4: error: Tactic `cases` failed: major premise type is not an inductive type
  α

Explanation: the `cases` tactic is for constructor-based reasoning as well as for applying custom cases principles with a 'using' clause or a registered '@[cases_eliminator]' theorem. The above type neither is an inductive type nor has a registered theorem.

α : Type u_1
A B : Set α
h : A ⊆ B
x : α
⊢ x ∈ A ∪ B → x
Wrong tactic
An automation or closing tactic ran and failed on this goal (linarith, omega, simp made no progress, …).
Example proof (mh_cate_9a8e08, Direct)
intro J
apply CategoryTheory.Limits.preserves_limits_of_yoneda
apply CategoryTheory.Limits.preserves_limits_of_essential_surjectivity
apply CategoryTheory.Limits.preserves_limits_of_subcanonical
exact J.Subcanonical
Lean output
4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

C : Type u
inst✝¹ : CategoryTheory.Category.{v, u} C
J : CategoryTheory.GrothendieckTopology C
inst✝ : J.Subcanonical
⊢ CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, v, max u v, u, max u (v + 1)} J.yoneda
Valid but mathematically wrong
The proof elaborates, but goals remain unsolved: well-formed Lean that does not prove the statement.
Example proof (novel_ineq_02, Direct)
have h1 : x + 1 / x = (x^2 + 1) / x := by ring
have h2 : x^2 + 1 ≥ 2 * x := by linarith [hx]
rw [h1]
apply div_le_of_le_mul_right hx
exact h2
Lean output
4:44: info: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
4:41: error: unsolved goals
x : ℝ
hx : 0 < x
⊢ x + x⁻¹ = x ^ 2 * x⁻¹ + x⁻¹
5:34: error: l
Timeout
Heartbeat or recursion limit, or the 60-second wall-clock backstop.
Example proof (mh_prob_51c110, Hybrid retrieval + repair)
have : HasSum (fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) 1 :=
  by
    let s := fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial
    let f := fun n => ↑r ^ n / ↑n.factorial
    have hf : HasSum f (Real.exp ↑r) :=
      by
        refine' hasSum_converges_of_radius _ _
        exact Real.exp_pos ↑r
        refine' hasSum_converges_of_radius _ _
        exact Real.exp_pos ↑r
        exact Real
Lean output
wall-clock timeout after 60s
Forbidden token
Rejected before compilation: `sorry`, `admit`, axioms, `native_decide`, `set_option`, metaprogramming or top-level commands.
Example proof (mh_numb_485b85, Direct ×4)
intro x; intro h;
have : ∀ n : ℕ, (fwdDiff 1)^[n] (⇑f) 0 = 0 := by
  induction' x with n h IH
  case zero => rfl
  case succ n =>
    have : (fwdDiff 1)^[n+1] (⇑f) 0 = 0 :=
      congrArg (fun f => (fwdDiff 1)^[n+1] f 0) (by simp [fwdDiff])
      sorry
    exact this
end
apply Filter.Tendsto_const
Lean output
rejected before compilation: forbidden token(s): sorry
No proof
The model's reply contained no tactic block.
Rejected by certifier
Passed the fast REPL check but the independent certifier rejected it: a banned premise, extra declarations, or non-standard axioms.
Example proof (mh_prob_7d2670, Full (plan + retrieval + repair))
-- Since X has a Gaussian law, it is integrable by the properties of Gaussian distributions.
-- In particular, Gaussian distributions on Euclidean spaces have finite moments of all orders.
-- We can use the fact that the integral of X with respect to P exists and is finite.
-- This follows from the lemma `ProbabilityTheory.HasLaw.integral_eq` which gives an explicit expression for the integral.
--
Lean output
The proof was rejected by the final checker: banned_premise:ProbabilityTheory.HasGaussianLaw.integrable
Other
Any Lean error the rules above do not match.
Example proof (mh_ineq_04b8ca, Direct)
rw [Set.Iic, Set.Iio]
apply_fun (fun x => x - 1) at hb
exact hb
Lean output
5:2: error: apply_fun can only handle negations of equality.