Zulip Chat Archive

Stream: general

Topic: Prime number theorem in lean


view this post on Zulip 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

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 14 2019 at 05:58):

why should those obscure combinations of letter represent PNT?

view this post on Zulip Kenny Lau (Jun 14 2019 at 05:59):

but nice job translating a language to another language I guess

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 14 2019 at 05:59):

did you use complex analysis?

view this post on Zulip Mario Carneiro (Jun 14 2019 at 05:59):

no

view this post on Zulip Mario Carneiro (Jun 14 2019 at 05:59):

it's the erdos-selberg proof

view this post on Zulip Mario Carneiro (Jun 14 2019 at 06:00):

obviously the next step is unfolding all the ZFC junk away

view this post on Zulip Mario Carneiro (Jun 14 2019 at 06:00):

so that it actually looks like the prime number theorem

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 06:02):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 14 2019 at 06:39):

It would

view this post on Zulip Mario Carneiro (Jun 14 2019 at 06:39):

this statement is equivalent, in lean, to PNT

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 14 2019 at 07:02):

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

view this post on Zulip Kenny Lau (Jun 14 2019 at 07:02):

sounds about right

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 07:02):

fair point

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 14 2019 at 07:13):

you're working on transfer now? :D

view this post on Zulip Mario Carneiro (Jun 14 2019 at 07:14):

by hand transfer, of course

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 08:10):

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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 08:14):

indeed it does

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 14 2019 at 08:38):

That sounds really exciting! Nice work!

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 09:06):

Hmm, I see that this proof uses deprecated axioms.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 09:17):

this is common for "construction" theorems/axioms

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 09:18):

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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 09:19):

and also run really really fast

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 14 2019 at 12:28):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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} := ...

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 05:30):

That's pretty awesome!

view this post on Zulip Johan Commelin (Jun 19 2019 at 05:32):

Wow! Congratulations!

view this post on Zulip Johan Commelin (Jun 19 2019 at 05:32):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 09:40):

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

view this post on Zulip Mario Carneiro (Jun 19 2019 at 09:41):

that's the hope

view this post on Zulip Mario Carneiro (Jun 19 2019 at 09:42):

for now this is just a proof of concept

view this post on Zulip 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)

view this post on Zulip 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'

view this post on Zulip Kenny Lau (Jun 19 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:08):

all of the same properties that real has

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:08):

like just name true things, they are all there

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:10):

no pun intended

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 10:23):

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

view this post on Zulip Kevin Buzzard (Jun 19 2019 at 10:24):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:36):

In this case, the reals are plenty overdetermined

view this post on Zulip Mario Carneiro (Jun 19 2019 at 10:36):

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

view this post on Zulip 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

view this post on Zulip Yao Liu (Jun 19 2019 at 13:57):

complete as "Dedekind complete", not Cauchy complete

view this post on Zulip Johan Commelin (Oct 24 2019 at 10:10):

@Tim Daly For example this thread

view this post on Zulip 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