Interest in contributing Chebyshev’s Theorem (PNT Precursor)

Stream: new members

[Ashton J]

Hello! This is my first time ever posting to this board.

I have been using Lean/Matlib for the past 2 years, and wanted to learn how to contribute.

Specifically, my most recent project has required me to re-formalize "Chebyshev’s Theorem" as a weaker form of the Prime Number Theorem. It is complete, it compiles and runs, but is perhaps a bit messier than I would like, and I am unaware of the style guides that official adoption requires.

I would love to learn how to contribute. I am an undergraduate student, and have little experience working with a community such as this.

I will refrain from posting the full code here now, as I am not sure if this is the best place to post this.

Thank you all for your hard work!

-Ashton

[Bryan Gin-ge Chen]

Welcome! We have a page on "How to contribute" on our website which includes a link to our style guide and naming conventions.

I'm afraid I can't answer specifically about Chebyshev's theorem -- maybe if you post just the type of the main theorem you'd like to add someone more familiar with analytic number theory in mathlib can point you to the right place to look.

[Ashton J]

Bryan Gin-ge Chen said:

Welcome! We have a page on "How to contribute" on our website which includes a link to our style guide and naming conventions.

I'm afraid I can't answer specifically about Chebyshev's theorem -- maybe if you post just the type of the main theorem you'd like to add someone more familiar with analytic number theory in mathlib can point you to the right place to look.

Thank you for the advice!

Interestingly enough, Chebyshev's theorem does not actually use analytic number theory, its purely elementary (pre-analytic). It uses combinatorics and binomials, it does not even use calculus.

[Aaron Liu]

are you referring to the statement that "if $\pi(n)\log(n)/n$ converges as $n \to \infty$, then it converges to one" there are a lot of chebyshev theorems

[Ashton J]

Aaron Liu said:

are you referring to the statement that "if $\pi(n)\log(n)/n$ converges as $n \to \infty$, then it converges to one" there are a lot of chebyshev theorems

I am referring to specifically Chebyshev's Theorem concerning the distribution of prime numbers, so a lower bound for the prime counting function: For sufficiently large n, π(n) ≥ c·n/log(n) for some explicit c > 0.

The theorem you referenced looks closer to the full PNT, while Chebyshev is a strictly weaker bound than the PNT.

Chebyshev:
$\pi(n) < c \frac{n}{\log n}$

so a way you can use it:

$0.921 \frac{n}{\log n} < \pi(n) < 1.106 \frac{n}{\log n}$

Prime Number Theorem:

$\lim_{n \to \infty} \frac{\pi(n) \log(n)}{n} = 1$

---

So Chebyshev is useful in the interim, as a full PNT formalization is... difficult.

[Aaron Liu]

oh ok that makes sense