## Stream: general

### Topic: Prime number theorem in lean

#### Mario Carneiro (Jun 14 2019 at 05:56):

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


#### Mario Carneiro (Jun 14 2019 at 05:57):

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 (Jun 14 2019 at 05:58):

why should those obscure combinations of letter represent PNT?

#### Kenny Lau (Jun 14 2019 at 05:59):

but nice job translating a language to another language I guess

#### Mario Carneiro (Jun 14 2019 at 05:59):

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

#### Kenny Lau (Jun 14 2019 at 05:59):

did you use complex analysis?

no

#### Mario Carneiro (Jun 14 2019 at 05:59):

it's the erdos-selberg proof

#### Mario Carneiro (Jun 14 2019 at 06:00):

obviously the next step is unfolding all the ZFC junk away

#### Mario Carneiro (Jun 14 2019 at 06:00):

so that it actually looks like the prime number theorem

#### Mario Carneiro (Jun 14 2019 at 06:01):

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 (Jun 14 2019 at 06:02):

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

#### Mario Carneiro (Jun 14 2019 at 06:10):

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 (Jun 14 2019 at 06:22):

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?

It would

#### Mario Carneiro (Jun 14 2019 at 06:39):

this statement is equivalent, in lean, to PNT

#### Mario Carneiro (Jun 14 2019 at 06:40):

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 (Jun 14 2019 at 07:00):

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

#### Kevin Buzzard (Jun 14 2019 at 07:02):

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 (Jun 14 2019 at 07:02):

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

fair point

#### Mario Carneiro (Jun 14 2019 at 07:13):

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 (Jun 14 2019 at 07:13):

you're working on transfer now? :D

#### Mario Carneiro (Jun 14 2019 at 07:14):

by hand transfer, of course

#### Kevin Buzzard (Jun 14 2019 at 08:10):

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

indeed it does

#### Mario Carneiro (Jun 14 2019 at 08:15):

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

#### Mario Carneiro (Jun 14 2019 at 08:17):

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 (Jun 14 2019 at 08:38):

That sounds really exciting! Nice work!

#### Kevin Buzzard (Jun 14 2019 at 09:06):

Hmm, I see that this proof uses deprecated axioms.

#### Kevin Buzzard (Jun 14 2019 at 09:06):

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 (Jun 14 2019 at 09:09):

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 (Jun 14 2019 at 09:11):

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 (Jun 14 2019 at 09:13):

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 (Jun 14 2019 at 09:16):

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

#### Mario Carneiro (Jun 14 2019 at 09:17):

this is common for "construction" theorems/axioms

#### Mario Carneiro (Jun 14 2019 at 09:18):

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 (Jun 14 2019 at 09:18):

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

#### Mario Carneiro (Jun 14 2019 at 09:19):

and also run really really fast

#### Mario Carneiro (Jun 14 2019 at 09:20):

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 (Jun 14 2019 at 09:21):

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 (Jun 14 2019 at 10:53):

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 (Jun 14 2019 at 12:25):

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 (Jun 14 2019 at 12:27):

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

#### Mario Carneiro (Jun 14 2019 at 12:28):

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

#### Jesse Michael Han (Jun 14 2019 at 13:07):

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 (Jun 14 2019 at 13:09):

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

#### Mario Carneiro (Jun 15 2019 at 00:06):

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 (Jun 19 2019 at 02:24):

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 (Jun 19 2019 at 02:26):

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 (Jun 19 2019 at 05:30):

That's pretty awesome!

#### Johan Commelin (Jun 19 2019 at 05:32):

Wow! Congratulations!

#### Johan Commelin (Jun 19 2019 at 05:32):

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

#### Mario Carneiro (Jun 19 2019 at 05:36):

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 (Jun 19 2019 at 09:40):

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

that's the hope

#### Mario Carneiro (Jun 19 2019 at 09:42):

for now this is just a proof of concept

#### Kenny Lau (Jun 19 2019 at 10:05):

@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 (Jun 19 2019 at 10:06):

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 (Jun 19 2019 at 10:08):

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

#### Mario Carneiro (Jun 19 2019 at 10:08):

all of the same properties that real has

#### Mario Carneiro (Jun 19 2019 at 10:08):

like just name true things, they are all there

#### Mario Carneiro (Jun 19 2019 at 10:09):

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

#### Mario Carneiro (Jun 19 2019 at 10:10):

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

no pun intended

#### Mario Carneiro (Jun 19 2019 at 10:12):

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

#### Kevin Buzzard (Jun 19 2019 at 10:22):

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 (Jun 19 2019 at 10:24):

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

#### Kevin Buzzard (Jun 19 2019 at 10:25):

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 (Jun 19 2019 at 10:36):

In this case, the reals are plenty overdetermined

#### Mario Carneiro (Jun 19 2019 at 10:36):

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

#### Yao Liu (Jun 19 2019 at 13:56):

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 (Jun 19 2019 at 13:57):

complete as "Dedekind complete", not Cauchy complete

#### Johan Commelin (Oct 24 2019 at 10:10):

@Tim Daly For example this thread

#### Mario Carneiro (Oct 25 2019 at 00:35):

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

Last updated: May 08 2021 at 04:14 UTC