Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target : IsTrans ℕ fun a b => b + 2 ≤ a := by

Mathlib declaration: instIsTransNatLeHAddOfNat
Held-out module: Mathlib.Data.Nat.Fib.Zeckendorf
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 3 / 0

Traces

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

Not verified1 model calls · 1 Lean checks · $0.00006

Attempts

sample 0 · round 0Lean 3 syntax2.9 s model time

Proof

intro a b c
assume h1 : b + 2 ≤ a
assume h2 : c + 2 ≤ b
have h3 : c + 2 + 2 ≤ a := add_le_add_right h2 2
rw [add_assoc] at h3
exact h3

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

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

⊢ IsTrans ℕ fun a b => b + 2 ≤ a
5:12: error: unexpected token ':'; expected command

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

@[nolint docBlame]
local instance : IsTrans ℕ fun a b ↦ b + 2 ≤ a where
  trans _a _b _c hba hcb := hcb.trans <| le_self_add.trans hba