Theorems / mh_numb_ca43f0

Mathlib held-out

Number theory · hard

Statement, exactly as the model and Lean see it
theorem lg_target {x : ℝ} (hx : 1 < x) : ↑⌊x⌋₊.primeCounting ≤ Real.log 4 * x / Real.log √x + √x := by
Mathlib declaration
Chebyshev.pi_le_log4_mul_div
Held-out module
Mathlib.NumberTheory.Chebyshev
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
89 / 3

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

Attempts

  1. sample 0 · round 0Lean 3 syntax59.5 s model time
    Proof
    ```lean
intro x
have h1 : 0 < x := lt_trans (lt_iff_pos_left.2 (le_of_gt hx)) (lt_zero_neg (neg_pos.mpr hx))
have h2 : 0 < Real.log √x := log_pos (pow_pos (real.sqrt_pos h1) 2)
let n := ⌊x⌋₊
have h3 : n ≤ x := le_floor_iff.1 (le_rfl)
have h4 : n ≥ 1 := le_antisymm (le_zero (real.floor_le x)) (le_of_gt hx)
have h5 : Real.log 4 * x / Real.log √x + √x = Real.log 4 * x / Real.log √x + Real.sqrt x :=
  rfl
have h6 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  add_nonneg (le_refl _) (le_zero_real_sqrt h1)
have h7 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h6
have h8 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h7
have h9 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h8
have h10 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h9
have h11 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h10
have h12 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h11
have h13 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h12
have h14 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h13
have h15 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h14
have h16 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h15
have h17 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h16
have h18 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h17
have h19 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h18
have h20 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h19
have h21 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h20
have h22 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h21
have h23 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h22
have h24 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h23
have h25 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h24
have h26 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h25
have h27 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h26
have h28 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h27
have h29 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h28
have h30 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h29
have h31 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h30
have h32 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h31
have h33 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h32
have h34 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h33
have h35 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h34
have h36 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h35
have h37 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h36
have h38 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h37
have h39 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h38
have h40 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h39
have h41 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h40
have h42 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h41
have h43 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h42
have h44 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h43
have h45 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h44
have h46 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h45
have h47 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h46
have h48 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h47
have h49 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h48
have h50 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h49
have h51 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h50
have h52 : Real.log 4 * x / Real.log √x + Real.sqrt x ≥ Real.log 4 * x / Real.log √x :=
  h5
    What Lean printed (this is all the model sees on repair)
    3:100: error: unsolved goals
x : ℝ
hx : 1 < x
⊢ ↑⌊x⌋₊.primeCounting ≤ Real.log 4 * x / Real.log √x + √x
4:2: 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.

/-- A weak but completely explicit upper bound on $\pi(x)$. -/
theorem pi_le_log4_mul_div {x : ℝ} (hx : 1 < x) : π ⌊x⌋₊ ≤ log 4 * x / log √x + √x := by
  have : 0 < log √x := log_pos (lt_sqrt_of_sq_lt (by simp [hx]))
  field_simp
  grind [pi_mul_log_sqrt_le hx.le]