Research proof index

An explicit upper bound for the number of primes below $N$: $|\{p<N:p\text{ is prime}\}|\le \frac{4N}{\log N}+6\sqrt N\left(1+\frac12\log N\right)^3.$ The formal statement also covers the small values of $N$ using Lean's totalized real operations.

A prime number theorem in arithmetic progressions, in Chebyshev-weighted form. If $q\ge1$, $a<q$, and $\gcd(a,q)=1$, then $\sum_{\substack{p\le x\\p\equiv a\pmod q}}\log p\sim\frac{x}{\varphi(q)}$ as $x\to\infty$.

At every point $p\in\mathbb C$, the axis-parallel closed squares centered at $p$ with positive half-width form a neighborhood basis. Equivalently, a set is a neighborhood of $p$ exactly when it contains one of these sufficiently small squares.

Dirichlet's theorem on primes in arithmetic progressions. If $q\ge 1$, $a<q$, and $\gcd(a,q)=1$, then infinitely many primes satisfy $p\equiv a\pmod q$.

For every integer $n\ge0$, the corrected harmonic approximation $H_{n+1}-\log(n+1)-\frac{1}{2(n+1)}$ is a lower bound for the Euler–Mascheroni constant $\gamma$.

Let $E_\pi(x)=|\pi(x)-\operatorname{Li}(x)|/(x/\log x)$. If $E_\pi$ obeys the classical bound $E_\pi(x)\le A\left(\frac{\log x}{R}\right)^B\exp\!\left(-C\sqrt{\frac{\log x}{R}}\right)$ for every $x\ge x_0$, with $A,B,C,R>0$, then beyond any $x_1\ge\max\{x_0,\exp(R(2B/C)^2)\}$ it obeys the uniform numerical bound obtained by evaluating that expression at $x_1$.