Introduction to Formalization

Originally, when proof assistants and theorem provers were being invented, they were intended to be used to verify the correctness of computer programs, but it soon became clear that the technology at the core of these systems could be used to verify human proofs of mathematical theorems. Despite the fact that historically, mathematicians have been resistant to using these technologies, the growing popularity of experimental mathematics and the use of proof assistants gives credence to the idea that one day mathematicians and computers can live symbiotically for the advancement of science and mathematics as a whole.

More text ...

More text ...

The Riemann Hypothesis

The problem of classifying the non-trivial zeroes of the Riemann Zeta Function has remained unsolved for more than 160 years. It has far reaching consequences for number theory, but more than that, the search for a solution has fostered the development of new techniques and theories, as many important problems of mathematics do. In the spirit of what the Riemann Hypothesis (RH) gave to mathematics and what proof assistants and algorithmic reasoning will give to mathematics in the future, we have formalized RH inside of the Lean Theorem Prover.

AbsoluteValue -> CauchySequence -> ℝ & ℂ -> Dirichlet η -> Riemann Hypothesis

Implementation Docs

What follows is the user-interface to the RH implementation, including the relevant definitions, lemmas, theorems, ... etc. which can be used to write statements and proofs about RH and its related concepts. The library tries to use mathlib to the least extent possible, but still requires some definitions from the tactic, algebra, and analysis libraries. See the source implementation for more details.

Absolute Value
file: src/absolute_value.lean

Dirichlet Eta
file: src/dirichlet_eta.lean

dirichlet_eta.partial_sum.is_cauchy (s : ℂ) (σpos : 0 < σ)
    : is_cauchy complex_abs (dirichlet_eta.partial_sum s)
    :=  impl 

dirichlet_eta.cauchy_sequence (s σpos)
    : CauchySequence complex_abs
    := { sequence         := dirichlet_eta.partial_sum s,
         cauchy_condition := dirichlet_eta.partial_sum.is_cauchy s σpos }

dirichlet_eta (s σpos)
    := (dirichlet_eta.cauchy_sequence s σpos).limit

Riemann Hypothesis
file: src/riemann_hypothesis.lean

riemann_hypothesis (s σpos)
    := dirichlet_eta s σpos = 0 → s.re = 1 / 2