Algebra · easy

Statement, exactly as the model and Lean see it

theorem lg_target (a b c : ℚ) (h₁ : a + b = 5) (h₂ : b + c = 7) (h₃ : a + c = 6) : a = 2 := by

Source: Written for LeanGraph, reference proof certified
Premises used by the reference proof: 51

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Verified0 model calls · 6 Lean checks · $0.00000

Attempts

attempt 1Wrong tactic

Proof

rfl

What Lean printed (this is all the model sees on repair)

4:2: error: Tactic `rfl` failed: The left-hand side
  a
is not definitionally equal to the right-hand side
  2

a b c : ℚ
h₁ : a + b = 5
h₂ : b + c = 7
h₃ : a + c = 6
⊢ a = 2

attempt 2Other

Proof

decide

What Lean printed (this is all the model sees on repair)

4:2: error: Expected type must not contain free variables
  a = 2

Hint: Use the `+revert` option to automatically clean up and revert free variables

attempt 3Valid but mathematically wrong

Proof

norm_num

What Lean printed (this is all the model sees on repair)

3:92: error: unsolved goals
a b c : ℚ
h₁ : a + b = 5
h₂ : b + c = 7
h₃ : a + c = 6
⊢ a = 2

attempt 4Wrong tactic
Proof
```
simp
```
What Lean printed (this is all the model sees on repair)
```
4:2: error: `simp` made no progress
```

attempt 5Wrong tactic

Proof

ring

What Lean printed (this is all the model sees on repair)

4:2: 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.
3:92: error: unsolved goals
a b c : ℚ
h₁ : a + b = 5
h₂ : b + c = 7
h₃ : a + c = 6
⊢ a = 2

attempt 6Verified
Proof
```
linarith
```

Verified proof

theorem lg_target (a b c : ℚ) (h₁ : a + b = 5) (h₂ : b + c = 7) (h₃ : a + c = 6) : a = 2 := by
  linarith

Axioms used: propext, Classical.choice, Quot.sound

Reference proof

The proof we wrote and certified before any model ran.

linarith