Number theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : 6 ∣ n * (n + 1) * (n + 2) := by

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

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.00010

Attempts

sample 0 · round 0Hallucinated theorem4.5 s model time

Proof

have h1 : 2 ∣ n * (n + 1) * (n + 2) := dvd_mul_of_dvd_left (dvd_mul_of_dvd_right (dvd_mul_of_dvd_left (dvd_two 2) (dvd_two 2)) (dvd_two 2))
have h2 : 3 ∣ n * (n + 1) * (n + 2) := dvd_mul_of_dvd_left (dvd_mul_of_dvd_right (dvd_mul_of_dvd_left (dvd_three 3) (dvd_three 3)) (dvd_three 3))
exact dvd_mul_of_dvd_left h2 h1

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

4:105: error: Unknown identifier `dvd_two`
4:117: error: Unknown identifier `dvd_two`
4:130: error: Unknown identifier `dvd_two`
5:105: error: Unknown identifier `dvd_three`
5:119: error: Unknown identifier `dvd_three`
5:134: error: Unknown identifier `dvd_three`
6:31: error: Application type mismatch: The argument
  h1
has type
  2 ∣ n * (n + 1) * (n + 2)
of sort `Prop` but is expected to have type
  ℕ
of sort `Type` in the application
  dvd_mul_of_dvd_left h2 h1

Reference proof

The proof we wrote and certified before any model ran.

have h : n % 6 < 6 := Nat.mod_lt _ (by norm_num)
interval_cases hn : n % 6 <;> simp [Nat.dvd_iff_mod_eq_zero, Nat.mul_mod, Nat.add_mod, hn]