6
$\begingroup$

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

Improve this question
$\endgroup$
3
  • 7
    $\begingroup$ This might be better suited to the new Proof Assistants stackexchange, proofassistants.stackexchange.com $\endgroup$
    – Thomas Bloom
    Commented Sep 20, 2022 at 12:00
  • 2
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Sep 20, 2022 at 13:29
  • $\begingroup$ 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. $\endgroup$
    – Sylvain JULIEN
    Commented Sep 20, 2022 at 18:07

2 Answers 2

Reset to default
8
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ 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. $\endgroup$
    – Neil Strickland
    Commented Jul 25, 2023 at 19:35
  • $\begingroup$ 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 $\endgroup$
    – Sidharth Ghoshal
    Commented Jul 25, 2023 at 20:04
  • $\begingroup$ Pull requests for mathlib are scrutinised closely and required to adhere to extensive coding standards. You can see details at leanprover-community.github.io/contribute/index.html $\endgroup$
    – Neil Strickland
    Commented Jul 25, 2023 at 21:28
4
$\begingroup$

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

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Commented Jul 22, 2023 at 15:29
  • $\begingroup$ @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? $\endgroup$
    – EGME
    Commented Jul 22, 2023 at 16:01
  • 1
    $\begingroup$ 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.) $\endgroup$
    – Emil Jeřábek
    Commented Jul 22, 2023 at 16:04
  • 1
    $\begingroup$ 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 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. $\endgroup$
    – Emil Jeřábek
    Commented Jul 22, 2023 at 17:25
  • 1
    $\begingroup$ @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. $\endgroup$
    – EGME
    Commented Jul 25, 2023 at 19:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .