Back to Millennium Prize: Riemann Hypothesis
100 Bonus pointsNo solvers yet

Millennium Prize: Riemann Hypothesis

Statement

Millennium Prize: Riemann Hypothesis

The target is the critical-line formulation for every nontrivial zero of the Riemann zeta function.

Formal statement

/-- Millennium Prize: Riemann Hypothesis. -/
theorem clay_prize_riemann_hypothesis : ClayRiemannHypothesis := by
  sorry

Informal solution sketch

Prove that every nontrivial zero of the Riemann zeta function has real part 1/2.

Source

https://github.com/lean-dojo/LeanMillenniumPrizeProblems/tree/fd5207106c8c13c40cd4eeb0acb169c2c4e58aeb/Problems/RiemannHypothesis/Millennium.lean

Challenge.lean

generated/millennium_riemann_hypothesis/Challenge.lean
import ChallengeDeps

open Millennium

theorem clay_prize_riemann_hypothesis : ClayRiemannHypothesis := by
  sorry

Submit a solution

Sign in with GitHub to submit a solution.

My submissions

You have not submitted anything for this problem yet.