Zulip Chat Archive

Stream: general

Topic: Leo's slides on Lean 4


view this post on Zulip Johan Commelin (Sep 03 2018 at 08:58):

Apropos Lean 4: Leo gave a new talk at Galois inc. You find the slides on leanprover.github.io: http://leanprover.github.io/talks/LeanAtGalois.pdf Some new information about Lean4!

What do the colors mean on slide 29?

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 09:06):

I guess blue are things implemented in C++, green for Lean, and red is external

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:08):

(deleted)

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 09:09):

On the second slide it says: "Lean is a platform for software verification and formalized mathematics"

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 09:10):

while software verification is highlighted mathematics is still mentioned...

view this post on Zulip Patrick Massot (Sep 03 2018 at 09:10):

but he was talking in front of people doing software verification

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:10):

He mentions Mario's ring tactic

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:10):

he hardly ever talks about mathlib

view this post on Zulip Johan Commelin (Sep 03 2018 at 09:11):

Kevin, he even mentions you!

view this post on Zulip Johan Commelin (Sep 03 2018 at 09:12):

The future of Lean 4 depends on you (-;

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:12):

He mentioned me in his Oxford talk. He believes in using Lean for education so it gets a mention. He is more skeptical about mathlib (he thinks it's too early) and in his Oxford talk he barely mentioned it at all.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:13):

On the other hand, ring is a really nice tactic, and Mario's recent edits to the tactic show that it really is not a trivial matter at all to get it working in Lean.

view this post on Zulip Johan Commelin (Sep 03 2018 at 09:14):

Well, I think that mentioning education is worth a lot more then pointing out: "Hey we've got our mathlib, which contains not even half of the stuff contained in other provers stdlibs"

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:14):

If he were to mention mathlib I think he'd do better by talking about the derivative of the size rather than the size.

view this post on Zulip Johan Commelin (Sep 03 2018 at 09:14):

The education thingy is pretty spectacular. And if it is a success, then a successful mathlib is a corollary.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:17):

And in some sense I'd like to take issue with this "maths library too small" comment. So we don't have Godel's incompleteness theorem. But we do have schemes and hence we have stuff taught at MSc level in a normal mathematics department. And soon we'll have perfectoid spaces and hence we will have stuff taught at PhD level in a strong mathematics department. I would be interested to see a list of topics which are in other theorem provers and which are introduced only at beginning graduate student level in a strong mathematics department in a mainstream (i.e. geometry, number theory, topology, algebra, analysis) course.

view this post on Zulip Mario Carneiro (Sep 03 2018 at 09:18):

External contributors can prove the new compiler is correct

See, he did mention me

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:18):

Leo told me I need to go into schools. He is really serious about the idea. I have one school talk in my calendar in October and I will almost certainly be doing another one before the end of the year.

view this post on Zulip Mario Carneiro (Sep 03 2018 at 09:21):

also, he's revealing quite a bit about lean 4 internals stuff, like the new lean IR. This is the first public appearance of it, so I guess he thinks it's pretty stable at this point

view this post on Zulip Simon Hudon (Sep 03 2018 at 16:04):

@Mario Carneiro What do you think of the promise of better support for proofs by reflection?

view this post on Zulip Mario Carneiro (Sep 03 2018 at 21:13):

I think it's great. Jeremy and I have talked before about an analogue to Coq's vm_compute, i.e. using #eval to prove theorems. This is sorely needed in many places, i.e. you can easily prove primality of 10 digit numbers using #eval but it is nearly impossible to use the decidable instance in the kernel. Obviously using #eval to prove things means that your trusted code base must include the entire compiler and associated things, but lean 4 is opening up the possibility of proving that all correct anyway, plus even an unverified computation is far more trustworthy than a human calculation, so I'm not particularly worried about inconsistency.

view this post on Zulip Mario Carneiro (Sep 03 2018 at 21:28):

One thing you can do today to emulate vm_compute is to normalize a term in the VM, then assert the equality as an axiom or use sorry. This has some obvious downsides though, since you can exploit these axioms to prove false things if you circumvent the tactic, i.e. it's not really checked for correctness. Doing this inside Lean would prevent the possibility for exploitation outside bugs in lean itself.

view this post on Zulip Simon Hudon (Sep 04 2018 at 04:19):

What worries me is that if we use this kind of feature, we may not have a choice to trust a lot of software. If one of our libraries use it, everything downstream won't be able to check using a small kernel


Last updated: May 18 2021 at 17:44 UTC