Prime number theorem

Stream: Is there code for X?

[Meow]

What is the current progress towards the prime number theorem, or a weaker sense, the Mertens formula in Lean?

[Meow]

In Isabelle there is a proof for Mertens formula using elementary methods. And more, with $L(s,\chi)\neq 0$ for non-principle characters, it is enough to prove the infinitude in arithmetic progressions (but much weaker than a prime number theorem).

[Johan Commelin]

Afaik, nobody is actively working on a Lean proof of PNT.

[Johan Commelin]

I would be inclined to use @Mario Carneiro's deep embedding of metamath into Lean. Not sure how we might/would/should want to tie that to mathlib. I personally would be in favour of a src/binary/ folder where we can dump those deep embeddings, and a subfolder src/binary/align that aligns stuff with the rest of mathlib. And then just transport metamath's PNT to Lean.

[Meow]

Thanks. How can I find these code for using deep embeddings?

[Johan Commelin]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean

[Meow]

It's not strange that Metamath can be embedded in Lean. The consistency strength of CIC is $\text{ZFC}+\omega \text{ inaccessible cardinals}$, so Metamath without Tarski-Grothendieck axiom can be embedded into it.

[Meow]

The Tarski-Grothendieck axiom needs a Mahlo cardinal and Lean doesn't have enough consistency strength.

[Meow]

What's more, parsing Metamath proofs are ratherly easy (I ever have written a parser, but remain unpublished), and the only difficulty is to convert Metamath "axioms" into Lean definitions. In contrast, it's harder to get Isabelle proof terms.

[Joseph Myers]

While I take a maximalist view of what's appropriate for mathlib (pretty much anything that could be considered known mathematics, from the mathematical sciences as a whole, is appropriate for mathlib or the mathlib archive if properly integrated with mathlib and following its coding standards, with the choice between mathlib and the mathlib archive being based on whether the material is likely to be reused or is very specific to a given result) - so that, for example, various projects people have done to prove some result or develop some theory outside of mathlib ought to end up in mathlib - this sort of proof converted from Metamath via a deep embedding is one of the things that seems less suitable to me (and likewise anything involving a large amount of auto-generated code not suitable for editing and maintaining by hand). The main benefit of PNT in Lean, as with many big results, would probably be the theory and lemmas developed to prove it rather than the result itself (although certainly the result itself is useful), and you don't get that benefit with such a proof converted from Metamath.

[Mario Carneiro]

I do think there is a gap here, where we don't have any process for making use of external proofs similar to FFI in programming languages. Especially big formalization projects can't always be done in one system due to organizational constraints - Flyspeck being one famous example, being written in HOL light and Isabelle - and I think we should work on having seamless integration between libraries. I don't think that we should be literally checking in a copy of translated-set.mm to mathlib, that would not fit our development model at all, but we should be able to depend on translated-set.mm for formalizations.

[Mario Carneiro]

The main benefit of PNT in Lean, as with many big results, would probably be the theory and lemmas developed to prove it rather than the result itself (although certainly the result itself is useful), and you don't get that benefit with such a proof converted from Metamath.

Of course. But maybe you are building a proof of something else and want to have PNT as a dependency without going into the details of the proof because they aren't relevant.

[Meow]

These viewpoints are interesting. However, in my opinion, I don't have a "maximalist" view for mathlib - in my view Lean is just one theorem prover, and not so speical.

[Meow]

For me, the most important problem of directly translating PNT to Lean is, it is a prove based on Selberg-Erdos method and not Riemann zeta function. This meant more precise estimation of the remainder item to be impossible.

[Mario Carneiro]

I think you misunderstood what Joseph was saying there. The "maximalist" view is about whether X mathematics is in scope for mathlib or not, not how mathlib relates to other theorem prover libraries

[Meow]

So the "maximalist" view is, all concurrent math is suitable to exist in mathlib?

[David Loeffler]

By "concurrent", do you just mean "current"?

[Meow]

David Loeffler said:

By "concurrent", do you just mean "current"?

Yes, that's a typo.

[Mario Carneiro]

Meow said:

For me, the most important problem of directly translating PNT to Lean is, it is a prove based on Selberg-Erdos method and not Riemann zeta function. This meant more precise estimation of the remainder item to be impossible.

I actually agree with this (despite being the original author of the metamath PNT proof). I think it would be more on-point for mathlib to formalize the abstract nonsense proof of PNT because it has better connections to other parts of abstract number theory which are of research interest. A proof of the PNT on it's own just isn't that much of an achievement anymore and the Erdos-Selberg proof won't pay many other dividends than PNT itself.

[David Loeffler]

I've never heard of complex analysis being described as "abstract nonsense" before! But I think we are all in agreement here that a Riemann-zeta-based proof written directly in Lean would be preferable over either (a) a proof via Erdos--Selberg, or (b) an incomprehensible hairball autotranslated from some other system (at which point it hardly matters what argument was used in the other system originally).

[Mario Carneiro]

as ever, I will reject the claim that the proof is incomprehensible though. It is actually a pretty direct translation of the original code, it would not be that bad to make it as presentable as the original proof

[Mario Carneiro]

TBH lean itself produces much worse proofs on its own

[Mario Carneiro]

More than anything else, I find the mentality harmful for translations generally, by denigrating the results as though it's not as good as a "real" proof. It serves a different purpose than source to source translations, that's all.

[Mario Carneiro]

As we have seen with the port, source to source translations have a host of other problems to deal with, and are generally much more resource-intensive

[David Loeffler]

I'm sorry, I meant no slight on your work (either the original achievement of proving PNT in Metamath, or that of writing the Metamath-to-Lean translator, both of which are pretty cool.)

[David Loeffler]

But I think we are not so far from being able to prove PNT directly. with the classical O(exp(sqrt log x)) error term, in mathlib. This is one of the motivations for the work that Meow and I have been doing to prove analytic continuation of Riemann zeta.

[Meow]

David Loeffler said:

But I think we are not so far from being able to prove PNT directly. with the classical O(exp(sqrt log x)) error term, in mathlib. This is one of the motivations for the work that Meow and I have been doing to prove analytic continuation of Riemann zeta.

Yes.

[David Loeffler]

At least, it was one of my motivations, and I'm glad to hear that it also seems to be one of yours :smile:

[Meow]

By the way, I don't regard Lean as the "best" tool for formalizing all mathematics. Some statements in mathematical logic may be more suitable to be formalized in Isabelle? Isabelle has two levels of logic, meta-level and object-level. In Isabelle we have many object-logics, for example, LCF, modal logic and sequent calculus.

[Meow]

But CIC can also be used as a meta-logic, similar to Isabelle/Pure. That's what model_theory do.

[Meow]

David Loeffler said:

At least, it was one of my motivations, and I'm glad to hear that it also seems to be one of yours :smile:

Thanks.

[Alex Kontorovich]

I'm glad to see renewed interest in PNT; ever since this project: https://github.com/bhgomes/lean-riemann-hypothesis (giving continuation of zeta to Re(s)>0 via alternating sums, in order to state RH via complex zeros), I've been hoping for there to be enough complex analysis to take a Mellin transform of a theta function (and thus define the actual "Riemann" zeta function...). @David Loeffler -- you're saying we're now getting close to that possibility? Fascinating!...

[David Loeffler]

@Alex Kontorovich Yes, it's definitely within reach: we have the transformation law for $\theta(-1/z)$, and from there, it's just a matter of taking a Mellin transform of that and checking all the integrals converge ok. @Meow was looking at that -- any thoughts?

[Alex Kontorovich]

Wow, how do we have the theta transformation law?? @Heather Macbeth and I have been (slowly) working up to Poisson summation, but maybe someone's beaten us to it?...

[Alex Kontorovich]

Also, will we be able to pull contours...? Thanks!

[Vincent Beffara]

Contour integrals (and the residue formula, and meromorphic functions) would be cool to have! I proved some variants of the Hurwitz theorem without that, going through local versions using integrals along small circles, along the way to the Riemann mapping theorem but it feels a bit artificial...

[David Loeffler]

@Heather Macbeth and I have been (slowly) working up to Poisson summation, but maybe someone's beaten us to it?

Yes: #18143 proves Poissson summation for a function on the real line such that both $f$ and $\hat{f}$ are continuous with exponential decay at infinity.

[David Loeffler]

Also, will we be able to pull contours...? Thanks!

Not sure what you mean there? The only role for contour integration in this argument is the evaluation of the Fourier transform of the Gaussian (contributed by @Meow) which uses a contour integral around a rectangular box. AFAIK we don't have integration around any more general contours currently (which is a major obstacle to developing modular forms, etc.)

[Vincent Beffara]

Yes AFAIK we only have rectangles and circles. Maybe it's time to think about more general contours?

[David Loeffler]

Maybe it's time to think about more general contours?

I think we would need to prove some version of the Jordan curve theorem in order to get the theory going (because you need to make sense of "inside" and "outside" the contour of integration)

[Vincent Beffara]

We can define the index without that, and possibly compute it in specific cases

[Vincent Beffara]

I would think that the Jordan curve theorem is really far away from what we have now

[Alex Kontorovich]

Didn't Hales formalize Jordan in Coq (?) like 15 years ago?... Why is it so far away?

[Alex Kontorovich]

Yes, here it is. (In HOL Light, not Coq) https://www.maths.ed.ac.uk/~v1ranick/papers/hales3.pdf

[Patrick Massot]

It shouldn't be so far away. But we are busy with porting to Lean 4.

[Mario Carneiro]

(I'm working on a project which might give us a terrible proof of the Jordan curve theorem sooner than expected...)

[Patrick Massot]

What is this project?

[Mario Carneiro]

not ready for the public

[Junyan Xu]

Simplicial homology and Brouwer's fixed point theorem have been formalized in Lean for a while. Certainly the Jordan curve theorem isn't (much) harder than Brouwer?

[Junyan Xu]

This is another nice account of the development of simplicial homology in HOL light: it also covers the Jordan-Schoenflies theorem (a strengthening of Jordan curve theorem that requires complex analysis) and the Jordan-Brouwer separation theorem (higher dimensional generalization).

[Sebastien Gouezel]

Once we have singular homology, Jordan and its higher-dimensional generalizations become easy. But for this we need a good homological formalism first, which should be backported from LTE, and this has to wait for after the port.

[Ruben Van de Velde]

Sebastien Gouezel said:

Once we have singular homology, Jordan and its higher-dimensional generalizations become easy. But for this we need a good homological formalism first, which should be backported from LTE, and this has to wait for after the port.

Stumbled upon this. Now that the port is over, what's the status? Has LTE been ported already / is anyone working on that?

[Andrew Yang]

There is an on-going refactor of the homology library. See https://leanprover.zulipchat.com/#narrow/stream/335062-homology/topic/Homology.20refactor.

[Adam Topaz]

We’re not porting LTE per se. But some parts are being moved directly to mathlib4