Lean 4

linarith failed to find a contradiction (Mathlib)

Q: What causes "linarith failed to find a contradiction (Mathlib)"?

The goal needs non-linear facts: products of variables, squares, division by a variable. A needed hypothesis is missing from the context, or hidden inside a definition linarith does not unfold. The goal is not an inequality or equation (for example ≠ or ∧). The statement is false as written.

Q: How do I confirm the cause?

Read the hypotheses in the message: the fact you need must be there, in linear form. Look for products, powers or divisions by variables — to linarith they are unrelated new variables. Try nlinarith; if it succeeds, the goal was non-linear.

Q: How do I fix "linarith failed to find a contradiction (Mathlib)"?

Give it the missing facts: linarith [h1, h2] accepts any proof terms, including lemma applications. For non-linear goals try nlinarith, or positivity for goals of the form 0 < e or 0 ≤ e. For ℕ and ℤ goals try omega, which also handles subtraction and division or modulo by constants. Split ∧ and ↔ goals with constructor before calling linarith.

Q: How do I stop it happening again?

State intermediate facts with have before calling linarith, so the final step is linear. Keep hypotheses as plain inequalities (a < b, a ≤ b) rather than buried in definitions.

Mathlib's linarith could not derive the goal from the hypotheses using linear arithmetic (adding and scaling inequalities).

What it looks like

Main.lean:3:2: error: linarith failed to find a contradiction
x y : ℝ
hx : 0 < x
hy : 0 < y
a✝ : 0 ≥ x * y
⊢ False
linarith failed to find a contradiction

What does "linarith failed to find a contradiction (Mathlib)" mean?

linarith (from Mathlib) negates the goal, adds it to the hypotheses and looks for a linear combination that gives a contradiction such as 0 < 0. When none exists it prints this message with the goal it was working on: ⊢ False, with your negated goal as the last hypothesis (a✝). It works over ordered fields such as ℚ and ℝ, and on ℕ and ℤ after some preprocessing, but it treats a product such as x * y as a single unknown.

What causes "linarith failed to find a contradiction (Mathlib)"?

The goal needs non-linear facts: products of variables, squares, division by a variable.
A needed hypothesis is missing from the context, or hidden inside a definition linarith does not unfold.
The goal is not an inequality or equation (for example ≠ or ∧).
The statement is false as written.

How do I confirm the cause?

Read the hypotheses in the message: the fact you need must be there, in linear form.
Look for products, powers or divisions by variables — to linarith they are unrelated new variables.
Try nlinarith; if it succeeds, the goal was non-linear.

How do I fix "linarith failed to find a contradiction (Mathlib)"?

Give it the missing facts: linarith [h1, h2] accepts any proof terms, including lemma applications.
For non-linear goals try nlinarith, or positivity for goals of the form 0 < e or 0 ≤ e.
For ℕ and ℤ goals try omega, which also handles subtraction and division or modulo by constants.
Split ∧ and ↔ goals with constructor before calling linarith.

How do I stop it happening again?

State intermediate facts with have before calling linarith, so the final step is linear.
Keep hypotheses as plain inequalities (a < b, a ≤ b) rather than buried in definitions.

Got a different error? Paste it into the Explain This Error tool → Identifies the family and the fix — runs locally, nothing uploaded.