Theorems / mh_numb_4094ce
Mathlib held-out
Number theory · hard
theorem lg_target {k : ℕ} {x : ℝ} (hk : k ≠ 0) (hx : x ∈ Set.Icc 0 1) : HurwitzZeta.hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1))) := by- Mathlib declaration
- HurwitzZeta.hurwitzZeta_neg_nat
- Held-out module
- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
- Banned modules (itself + downstream)
- 13
- Reference proof premises (reachable / held-out)
- 53 / 2
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.00031
Attempts
- sample 0 · round 0Syntax error12.9 s model time
Proof rw [HurwitzZeta.hurwitzZeta_def, Finset.sum_neg_succes, Finset.sum_const, Nat.cast_add, add_right_comm, mul_assoc, ←mul_one, ←Polynomial.map_C_eq_algebraMap, Polynomial.eval_map, Polynomial.bernoulli_neg_succ, ←Nat.cast_inj_iff.mp hk, ←Nat.cast_add, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one, ←Nat.cast_one,......
What Lean printed (this is all the model sees on repair) 4:1751: error: unexpected token '...'; expected ']' 4:6: error: Unknown identifier `HurwitzZeta.hurwitzZeta_def` 3:214: error: unsolved goals k : ℕ x : ℝ hk : k ≠ 0 hx : x ∈ Set.Icc 0 1 ⊢ HurwitzZeta.hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
/-- Values of Hurwitz zeta functions at (strictly) negative integers.
TODO: This formula is also correct for `k = 0`; but our current proof does not work in this
case. -/
theorem hurwitzZeta_neg_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
hurwitzZeta x (-k) =
-1 / (k + 1) * ((Polynomial.bernoulli (k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ) := by
rcases Nat.even_or_odd' k with ⟨n, (rfl | rfl)⟩
· exact_mod_cast hurwitzZeta_neg_two_mul_nat (by lia : n ≠ 0) hx
· exact_mod_cast hurwitzZeta_one_sub_two_mul_nat (by lia : n + 1 ≠ 0) hx