Back to Projects
ChallengeResearch100 pts on offer
Millennium Prize: Riemann Hypothesis
The target is the critical-line formulation for every nontrivial zero of the Riemann zeta function.
Overview
Millennium Prize: Riemann Hypothesis
millennium_riemann_hypothesis — a formalization challenge imported from lixiang90/math-challenge-millennium in lean-eval comparator format.
Notes
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
How to submit
Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified.
Write your proof in Submission.lean (plus any local modules under Submission/).
Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.
Comparator configuration
- Solution module:
Solution - Theorems checked:
clay_prize_riemann_hypothesis - Permitted axioms:
propext,Quot.sound,Classical.choice
Submitted by lean-dojo/LeanMillenniumPrizeProblems contributors.