Prime number theorem in lean

Stream: general

[Mario Carneiro]

I finally got the PNT to typecheck in lean! It looks something like this right now:

import .set6

namespace mm0

#check pnt
-- pnt : ⊦ wbr (cmpt (λ v0, co c1 cpnf cioo) (λ v0, co (cfv (cv v0) cppi) (co (cv v0) (cfv (cv v0) clog) cdiv) cdiv)) c1 crli

#print axioms pnt
-- propext
-- classical.choice
-- quot.sound

end mm0

Source: https://github.com/digama0/mm0/tree/build/mm0-lean/mm0/set

[Mario Carneiro]

This states that the prime number theorem holds in an embedding of nat inside Set. The proof is about 6 files of 100000 lines each, imported wholesale from metamath

[Kenny Lau]

why should those obscure combinations of letter represent PNT?

[Kenny Lau]

but nice job translating a language to another language I guess

[Mario Carneiro]

They are definitions upon definitions; this version might be a bit more readable -> http://us2.metamath.org/mpeuni/pnt.html

[Kenny Lau]

did you use complex analysis?

[Mario Carneiro]

no

[Mario Carneiro]

it's the erdos-selberg proof

[Mario Carneiro]

obviously the next step is unfolding all the ZFC junk away

[Mario Carneiro]

so that it actually looks like the prime number theorem

[Mario Carneiro]

The definitions are actually the "right" ones, i.e. wa which is the internal name for /\ translates to and in lean, but the stuff with sets is still not very definitionally similar to nat

[Mario Carneiro]

also I didn't bother with notation, obviously; the notation systems aren't really compatible

[Mario Carneiro]

It still takes far less time to typecheck than mathlib (it's about a minute), despite being much larger, but I guess that's no surprise

[Kevin Buzzard]

I don't understand what's going on here. If I formalised pnt in Lean using nats, presumably this wouldn't be able to prove it? So what has actually happened?

[Mario Carneiro]

It would

[Mario Carneiro]

this statement is equivalent, in lean, to PNT

[Mario Carneiro]

there is some postprocessing to be done on the statement, but it's not that bad; in particular I don't need to know anything about the proof to translate the statement to lean-native

[Kevin Buzzard]

So we can have all the theorems of everything in metamath? Or isn't it so easy?

[Kevin Buzzard]

PNT

⊦ wbr (cmpt (λ v0, co c1 cpnf cioo) (λ v0, co (cfv (cv v0) cppi) (co (cv v0) (cfv (cv v0) clog) cdiv) cdiv)) c1 crli

there is some postprocessing to be done on the statement

[Kenny Lau]

I guess I can see log and div and div near the end

[Kenny Lau]

sounds about right

[Kevin Buzzard]

fair point

[Mario Carneiro]

It's literally a matter of notation and simp and a bit of transfer to clean up the statement. I'm working on it now

[Kenny Lau]

you're working on transfer now? :D

[Mario Carneiro]

by hand transfer, of course

[Kevin Buzzard]

So is this anything to do with the enigmatic "meta-math zero"?

[Mario Carneiro]

indeed it does

[Mario Carneiro]

MM0 is the intermediate language for the first translation of metamath into HOL and DTT like systems

[Mario Carneiro]

but this is mostly a side effect of other stuff. I wonder if we can up the lean count on the 100 theorems list

[Johan Commelin]

That sounds really exciting! Nice work!

[Kevin Buzzard]

Hmm, I see that this proof uses deprecated axioms.

[Kevin Buzzard]

http://us2.metamath.org/mpeuni/ax-mulf.html

Is a deprecated axiom one which was universally believed to be true until someone found a counterexample?

[Kevin Buzzard]

MM0 is the intermediate language for the first translation of metamath into HOL and DTT like systems

I've just read the readme for MM0 and it means absolutely nothing to me. Can you say something about what MM0 means to me in practice as a Lean user?

[Kevin Buzzard]

If we can now prove PNT in Lean, formalised in what I would regard as a "normal" way, then I am surely interested. But I don't know, and am not sure I care about, what a "specification" is. I am interested in what all this means in practice. Does my question make some kind of sense?

[Kevin Buzzard]

Here's a question. Can you give me some file prime_number_theorem.lean which I can compile on my computer using lean --make and which turns into a proof of what I would regard as a fully verified proof of PNT in Lean?

[Mario Carneiro]

Deprecated axioms have a constrained use; they should only be used via other theorems, i.e. behind an API barrier

[Mario Carneiro]

this is common for "construction" theorems/axioms

[Mario Carneiro]

I've just read the readme for MM0 and it means absolutely nothing to me. Can you say something about what MM0 means to me in practice as a Lean user?

Not much, at least for the short to medium term. It's not ready for public consumption

[Mario Carneiro]

The goal is to produce theorem verifiers that don't have bugs in them

[Mario Carneiro]

and also run really really fast

[Mario Carneiro]

Here's a question. Can you give me some file prime_number_theorem.lean which I can compile on my computer using lean --make and which turns into a proof of what I would regard as a fully verified proof of PNT in Lean?

That would be set6.lean in the link above

[Mario Carneiro]

You probably won't regard it as a proof of PNT though, because it's completely unreadable. But I assure you that behind the notational mess is the correct theorem, and the actual proof is currently checkable in lean

[Reid Barton]

but this is mostly a side effect of other stuff. I wonder if we can up the lean count on the 100 theorems list

Surely it would be easier to prove that the harmonic series diverges

[Mario Carneiro]

I think this is much faster if the goal is to bring lean up to metamath... I highlighted PNT but it's all of set.mm

[Mario Carneiro]

that said, this is closer to a "cool project" than a practical import to incorporate into mathlib or something

[Mario Carneiro]

Probably it should be treated as a separate library from mathlib (because it is)

[Jesse Michael Han]

are you invoking a lemma which says that PNT is true for omega in Set iff PNT is true for nat in Lean?

[Jesse Michael Han]

it would be nice if we could uniformly transfer statements (like how eta < eta' iff their ordinal.mk's are < in Set)

[Mario Carneiro]

Yes, but keep in mind that all the facts that one would want about, say, nat in Set are already proven, i.e. there is a + and * and succ and succ is injective etc etc. So it's a matter of defining a map from one type to the other and applying the existing lemmas to see that the map preserves everything

[Mario Carneiro]

Success! For a slightly easier translation goal, I unmangled Dirichlet's theorem (which is just a statement about natural numbers). See https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/post.lean#L539 . The statement now makes no reference to MM0 definitions, that is, the statement is entirely "lean-native", although the proof isn't.

theorem dirith' {n : ℕ} {a : ℤ} (n0 : n ≠ 0) (g1 : int.gcd a n = 1) :
  ¬ set.finite {x | nat.prime x ∧ ↑n ∣ ↑x - a} := ...

[Mario Carneiro]

I think that post.lean is an interesting file to look at; it uses a combination of metamath and lean theorems to prove isomorphisms between the embedded ZFC world and the native lean world

[Kevin Buzzard]

That's pretty awesome!

[Johan Commelin]

Wow! Congratulations!

[Johan Commelin]

/me is very surprised that meta does not appear in that file.

[Mario Carneiro]

doing the PNT is harder because it involves logarithms and real numbers, so we need facts about the uniqueness of real which I think may not yet exist in lean

[Kevin Buzzard]

So will Lean soon be catching up with metamath on the list of 100 formal theorems?

[Mario Carneiro]

that's the hope

[Mario Carneiro]

for now this is just a proof of concept

[Kenny Lau]

@Mario Carneiro what sort of uniqueness of real do you need? I may be able to do it. (I had proved once that there is only one ring hom from R to R)

[Mario Carneiro]

Imagine you have another type real', with another exp', another log', and all the theorems you could want about them. Define a map from real to real' and prove that exp maps to exp' and log maps to log'

[Kenny Lau]

but what do you mean by another real'? What properties exactly does it have?

[Mario Carneiro]

all of the same properties that real has

[Mario Carneiro]

like just name true things, they are all there

[Mario Carneiro]

feel free to assume as many axioms as you like, as long as they speak exclusively about the primed versions of things

[Mario Carneiro]

if that turns out not to be true I have my work cut out for me as metamath maintainer, but metamath real numbers are a fair bit more complete than lean real numbers

[Mario Carneiro]

no pun intended

[Mario Carneiro]

As a starting point, it's a discrete linear ordered field with a supremum operation that satisfies the obvious properties

[Kevin Buzzard]

The reals are often inaccurately described as the unique complete totally ordered archimedean field, but there is certainly a theorem there. Patrick once dug out a Wikipedia link and we laughed at the ambiguity of it all.

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Real_number#%22The_complete_ordered_field%22 That was it.

[Kevin Buzzard]

The issue is that "complete" is a word used to mean several things in mathematics.

[Kevin Buzzard]

For me, archimedean is also an issue. For the reals it means basically that Z is unbounded in R, but in valuation theory a norm on a field is non-archimedean if it satisfies the weird strengthening of the triangle inequality |x+y!<=max(|x|,|y|), and is archimedean if it is not nonarchimedean. That might be a complete list of the pitfalls here.

[Mario Carneiro]

In this case, the reals are plenty overdetermined

[Mario Carneiro]

there are a half dozen theorems any of which would uniquely characterize it

[Yao Liu]

James Propp has an excellent article, Real Analysis in Reverse, that lists a number of equivalent "completeness axioms" https://arxiv.org/abs/1204.4483

[Yao Liu]

complete as "Dedekind complete", not Cauchy complete

[Johan Commelin]

@Tim Daly For example this thread

[Mario Carneiro]

For anyone who is interested, my CPP paper on Metamath Zero is now on arXiv: https://arxiv.org/abs/1910.10703