Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target (n : ℕ) : Real.log ↑(n + 1) ≤ ↑(harmonic n) := by

Mathlib declaration: log_add_one_le_harmonic
Held-out module: Mathlib.NumberTheory.Harmonic.Bounds
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 34 / 1

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

Attempts

sample 0 · round 0Wrong tactic3.0 s model time

Proof

intros n
rw [Real.log_add_one, Real.log_real]
apply Real.le_log_of_ge_one
apply Nat.succ_le_self
exact Nat.zero_le _

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

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

n : ℕ
⊢ Real.log ↑(n + 1) ≤ ↑(harmonic n)

Reference proof

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

theorem log_add_one_le_harmonic (n : ℕ) :
    Real.log ↑(n + 1) ≤ harmonic n := by
  calc _ = ∫ x in (1 : ℕ)..↑(n + 1), x⁻¹ := ?_
       _ ≤ ∑ d ∈ Finset.Icc 1 n, (d : ℝ)⁻¹ := ?_
       _ = harmonic n := ?_
  · rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by simp)]), div_one]
  · exact (inv_antitoneOn_Icc_right <| by simp).integral_le_sum_Ico (Nat.le_add_left 1 n)
  · simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]