Analytic Number Theory Exponent Database

License: Apache 2.0 Code Style: Black

This is the repository for the Analytic Number Theory Exponent Database (ANTEDB), an ongoing project to systematically record known theorems for various exponents appearing in analytic number theory, as well as the relationships between them. Currently, the database is recording facts and conjectures on exponent pairs, exponential sum bounds, zero-density and moment bounds for the Riemann zeta-function, large value estimates, additive energy bounds and exponents related to prime distributions, amongst other results (the full list of exponents can be found here). The database aims to organise and record theorems and relationships as both human-readable proofs and as executable python code. This builds upon the tables of exponent pairs and other related exponents that were collected in this paper of Trudgian and Yang, and aims to fulfil the vision set out in this blog post of Terence Tao.

This is intended to be a living database; additional corrections, updates, and contributions to the ANTEDB are welcome. Instructions for contributors can be found here.

Python database and proof automation

Each theorem and conjecture in the database is represented both in natural language and also in Python using the Hypothesis object. Each Hypothesis may either contain a reference to a result from the literature or depend on one or more other Hypothesis objects. The special predefined set literature contains all hypotheses of the first kind. For example, Ingham's 1940 zero-density estimate for the Riemann zeta function

is represented as a Hypothesis in literature, and can be retrieved using

import literature

h = literature.find_hypothesis(hypothesis_type="Zero density estimate", keywords="Ingham")
print("Hypothesis name:", h)
print("Hypothesis data:", h.data)
print("Hypothesis reference:", h.reference.title(), h.reference.author(), h.reference.year())
print("Hypothesis dependencies:", h.dependencies)

Console output

Hypothesis name: Ingham (1940) zero density estimate
Hypothesis data: A(x) \leq 3/(2 - x) on [1/2,1)
Hypothesis reference: {On} the estimation of ${N}(\sigma, T)$ Ingham 1940
Hypothesis dependencies: set()

There are no dependencies because this Hypothesis object directly references the literature. Alternatively, theorems may also be represented as a Hypothesis that (recursively) depend on other hypotheses. The dependency structure is a tree whose root is the theorem and whose leaves are other known theorems (either trivial or proved in the literature). This tree also represents a proof of the Hypothesis. For instance, we may also derive Ingham's estimate using other hypotheses in the database, such as large value estimates. This returns a Hypothesis object containing the same result but also containing a proof of the estimate represented as a dependency tree.

import derived

h = prove_zero_density_ingham_1940_v2()
h.recursively_list_proofs()

Console output

- [Derived zero density estimate]  i.e. A(x) \leq \frac{3 \left(x - 1\right)}{x - 2} on [1/2,1). Follows from computed large value estimates and zeta large value estimates with τ0 = 2 - σ for σ \in [1/2,1)). Dependencies:
        - [Derived large value estimate]  i.e. (σ,τ,ρ) in Disjoint union of {['-4/3 + 2/3σ + τ >= 0', '2 - σ - τ >= 0', '3/4 - σ >= 0', 'ρ >= 0', '-1/2 + σ >= 0', '2 - 2σ - ρ >= 0'], ['2 - σ - τ >= 0', '3/4 - σ >= 0', '-1/2 + σ >= 0', '1 - 2σ + τ - ρ >= 0', '-2 + 2σ + ρ >= 0']}. Follows from 1 large value estimates. Dependencies:
                - [Classical large value estimate]  i.e. ρ <= max(2 - 2σ, 1 - 2σ + τ). Classical.
        - [Derived zeta large value estimate]  i.e. (σ,τ,ρ) in Disjoint union of {['8/3 - 4/3σ + τ >= 0', '-2 + τ >= 0']}. Follows from 1 zeta large value estimates. Dependencies:
                - [Classical large value estimate]  i.e. ρ <= max(2 - 2σ, 1 - 2σ + τ). Classical.

The database also implements a limited automated theorem prover using known relationships between certain exponents in analytic number theory. A number of functions can be used to automatically find proofs given a desired result and a set of assumed Hypothesis. For example, to find a proof of the exponent pair , one can use

from exponent_pair import *

h = best_proof_of_exponent_pair(frac(4,18), frac(11,18))
h.recursively_list_proofs()

Console output

- [Derived exponent pair (2/9, 11/18)]  i.e. The exponent pair (2/9, 11/18). Follows from "Derived exponent pair (1/9, 13/18)" and taking the van der Corput B transform. Dependencies:
        - [van der Corput B transform]  i.e. van der Corput B transform. See [van der Corput, 1920]. 
        - [Derived exponent pair (1/9, 13/18)]  i.e. The exponent pair (1/9, 13/18). Follows from "Derived exponent pair (2/7, 4/7)" and taking the van der Corput A transform. Dependencies:
                - [van der Corput A transform]  i.e. van der Corput A transform. See [van der Corput, 1920].
                - [Derived exponent pair (2/7, 4/7)]  i.e. The exponent pair (2/7, 4/7). Follows from "Derived exponent pair (1/14, 11/14)" and taking the van der Corput B transform. Dependencies:
                        - [van der Corput B transform]  i.e. van der Corput B transform. See [van der Corput, 1920].
                        - [Derived exponent pair (1/14, 11/14)]  i.e. The exponent pair (1/14, 11/14). Follows from "Derived exponent pair (1/6, 2/3)" and taking the van der Corput A transform. Dependencies:
                                - [van der Corput A transform]  i.e. van der Corput A transform. See [van der Corput, 1920].
                                - [Derived exponent pair (1/6, 2/3)]  i.e. The exponent pair (1/6, 2/3). Follows from "Derived exponent pair (1/2, 1/2)" and taking the van der Corput A transform. Dependencies:
                                        - [van der Corput A transform]  i.e. van der Corput A transform. See [van der Corput, 1920].
                                        - [Derived exponent pair (1/2, 1/2)] i.e. The exponent pair (1/2, 1/2). Follows from "Trivial exponent pair (0, 1)" and taking the van der Corput B transform. Dependencies:
                                                - [van der Corput B transform]  i.e. van der Corput B transform. See [van der Corput, 1920].
                                                - [Trivial exponent pair (0, 1)]  i.e. The exponent pair (0, 1). Triangle inequality.