Analytic Number Theory Exponent Database
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.
- Main web page for this project.
- Web blueprint, containing a human-readable version of the database that is accessible online (see also the introduction here).
- Dependency graph of the theorems in the database.
- PDF form of blueprint, a downloadable, human-readable version of the database stored as a single file.
- Python code repository, containing a programmable version of this database and various optimization routines.
External links
- T. Tao, T. Trudgian, A. Yang, "New exponent pairs, zero density estimates, and zero additive energy estimates: a systematic approach": A paper describing the project, and several of the new results that already arose from it
- A blog post by Terence Tao describing this paper and project
- Mathbases - A directory of math databases (including this one)
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
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.