6

Might there be a research team that has formalised the Riemann Hypothesis? So far I have encountered two related questions:

  1. Is there a formulation of the Riemann Hypothesis in first-order arithmetic?

  2. Can the Riemann Hypothesis be undecidable?

A Google search reveals that the Prime Number Theorem has been formalised in HOL-light so it is reasonable to infer that the Riemann Hypothesis has been formalised [3]. If so, might there be a publication that analyses the different trade-offs that were involved?

References:

  1. Marc Larsson et al. Coqtail. 2022. Github repository. https://github.com/coq-community/coqtail-math

  2. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coqueliquot: A user-friendly Library for Real Analysis for Coq. 2015.

  3. John Harrison. HOL light: an overview. 2009. https://www.cl.cam.ac.uk/~jrh13/slides/tphols-18aug09/slides.pdf

Aidan Rocke
  • 3,827
  • 7
    This might be better suited to the new Proof Assistants stackexchange, https://proofassistants.stackexchange.com/ – Thomas Bloom Sep 20 '22 at 12:00
  • 2
    What exactly do you mean by formalizing the Riemann hypothesis? In the case of the prime number theorem, this simply means that it has been proven in the proof assistant, and this is common terminology. But RH remains unproven. – Emil Jeřábek Sep 20 '22 at 13:29
  • For what it's worth: I e-mailed someone from the INRIA years ago about the possibility to formalize my sketch of approach to RH, but got no news. – Sylvain JULIEN Sep 20 '22 at 18:07

2 Answers2

8

I just learned of the following formalisation led by Brandon Gomes and Alex Kontorovich from Andrej Bauer(via email):

Brandon Gomes & Alex Kontorovich. Formalization of the Riemann Hypothesis in the Lean Theorem Prover. Github repository. 2020. https://github.com/bhgomes/lean-riemann-hypothesis

Aidan Rocke
  • 3,827
  • 1
    You should note that the above repository is not part of mathlib and has not been updated for three years. As mathlib makes frequent changes that are not backwards-compatible, the repository will certainly not work with the current version. In principle it is possible to check out an old version of mathlib as specified in the leanpkg.toml file but that is not so satisfactory. – Neil Strickland Jul 25 '23 at 19:35
  • i assume "mathlib" is the main library. Is it hard to get things merged into there? Would it be difficult to translate this result and then try to merge it in – Sidharth Ghoshal Jul 25 '23 at 20:04
  • Pull requests for mathlib are scrutinised closely and required to adhere to extensive coding standards. You can see details at https://leanprover-community.github.io/contribute/index.html – Neil Strickland Jul 25 '23 at 21:28
4

Davis, Matijasevic, and Robinson show that RH is equivalent to the following arithmetic statement:

Let $$\delta(x)=\prod_{n<x}\prod_{j\leq n}\eta(j)$$

where $\eta(j)=1$ unless $j$ is a prime power, and $\eta(p^k)=p$ if $p$ is a prime number. Then

$$\left(\sum_{k\le\delta(n)}\frac{1}{k}-\frac{n^2}{2}\right)^2<36n^3$$ for $n\in\mathbb{N},n>0$.

This problem has also been translated into a halting problem by Matiyasevic, see reference [2] below.

Edit

It is interesting that RH might be independent of the theory that stems from the Peano Arithemtic axioms. Although the theory of the field of complex numbers is complete, and RH is formulated as a problem pertaining to complex numbers, as Emil Jeřábek points in his comment below, the FO theory of $\mathbb{C}$ is extremely weak to allow for even the definition of $\zeta$ in it.

Now, as Emil pointed out, I forgot to give an answer to the actual question in the post, regarding formalization (presumably in a proof assistant). A good amount of the analytic number theory leading to RH is formalized in Isabelle. It would be a nice exercise to complete this effort by adding the formalization of RH itself if it has not been done already; it should not be hard. See reference [3].

References

[1] Davis, M., Matijasevic, Y, and Robinson, J., Hilbert's tenth problem. Diophantine equations: positive aspects of a negative solution, in Proceedings of Symposia in Pure Mathematics: Mathematical developments arising from Hilbert problems, Vol XXVIII, Part 2, American Mathematical Socienty, Providence, Rhode Island, 1976.

The theorem appears on page 335.

[2] Matiyasevich, Y. The Riemann hypothesis in computer science, Theoretical Computer Science 807 (2020) 257-265

[3] Eberl, M. Nine chapters of analytic number theory in Isabelle/HOL, Technical University of Munich, accessed 25 July 2023: http://cl-informatik.uibk.ac.at/users/meberl/pdfs/ant.pdf

EGME
  • 1,018
  • 1
    Riemann Hypothesis cannot be formulated in the first-order language of the complex field. The structure of complex numbers endowed with the relevant machinery to support complex analysis, Dirichlet series, and the like, is even more complicated than Peano arithmetic; it is essentially second-order arithmetic. So properties of the theory of the mere complex field is completely irrelevant here. – Emil Jeřábek Jul 22 '23 at 15:29
  • @Emil Jeřábek. Correct. But you can define $\zeta$ in the critical strip in the first order language of $\mathbb{C}$ as follows: $\zeta(s)=\frac{1}{1-2^{1-s}}\sum_{n=1}^{\infty}\frac{(-1)^{n-1}}{n^s}$ (see Titchmarsh (2.2.1), this is due to Hardy). From there, the statement of RH in the FO language of $\mathbb{C}$ is straightforward (unless I am messing up the details). Is this not the case? – EGME Jul 22 '23 at 16:01
  • 1
    No, not at all. You cannot define anything resembling an infinite series without referring to integers. (Not to mention that exponentiation is not definable in the complex field either, hence you cannot even express the individual terms of your series.) – Emil Jeřábek Jul 22 '23 at 16:04
  • @Emil Jeřábek. Well, you have the integers in $\mathbb{C}$, but now I see maybe you do not get the full arithmetic with those in the FO theory of $\mathbb{C}$; thanks for pointing this out. I wonder how much you do get. – EGME Jul 22 '23 at 16:16
  • The integers are a subset of $\mathbb C$, but they are not first-order definable in the complex field. Almost nothing is: a subset of the complex field is first-order definable (even allowing arbitrary complex parameters) if and only if it is finite or cofinite. More generally, the only subsets of $\mathbb C^n$ that are first-order definable are Boolean combinations of algebraic sets. This extremely low expressive power is exactly what allows the theory of the complex field to be decidable in the first place. – Emil Jeřábek Jul 22 '23 at 16:22
  • @Emil Jeřábek. Ah, thank you for that wonderful and useful comment. This is now crystal clear. I will edit the question and point to your comment, while adding the reference to the formulation as a halting problem, which I just found. – EGME Jul 22 '23 at 16:27
  • 1
    All right. Now, the other issue is that this does not answer the question. The question asks for formalization (whatever exactly it means) of the Riemann Hypothesis in a theorem prover. The references here do not provide that. Rather, they prove that the Riemann Hypothesis is equivalent to particular arithmetic sentences (even $\Pi_1$), which makes this is a valid answer to https://mathoverflow.net/q/31846 (unless it is a duplicate, I didn’t check), not here. The OP specifically notes that he’s already aware of arithmetic equivalents of RH from the other question. – Emil Jeřábek Jul 22 '23 at 17:25
  • 1
    @EmilJeřábek. !! You are absolutely right. I have reading problems, so I tend to scan; my eyes fixated on the highlighted question right away. I will fix this. My answer is already included as an answer in MO/31846 (the first link takes you there). But I believe the second link might accomodate more in an answer. I have been looking into the formalization of RH anyway, in Isabelle. A substantial amount of the analytic number theory leading to RH has been formalized in Isabelle. I will at least add a reference to that effect now; later, more about this when I have time. – EGME Jul 25 '23 at 19:23