Zulip Chat Archive

Stream: general

Topic: Kevin's talk at MSR


view this post on Zulip Leonardo de Moura (Oct 01 2019 at 20:48):

Kevin's talk is finally available on YouTube: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

view this post on Zulip Daniel Selsam (Oct 09 2019 at 15:25):

Kevin's talk is on the front page of Hacker News: https://news.ycombinator.com/item?id=21200721

view this post on Zulip Reid Barton (Oct 09 2019 at 20:23):

I did my undergrad at Imperial. My first lecture was supposed to be with Prof. Liebeck. Kevin came in and wrote on the blackboard: "Lemma 1 - I am not professor Liebeck". He was wearing his (I think typical) trousers.

view this post on Zulip Andrew Ashworth (Oct 10 2019 at 14:56):

Somebody has raised an issue about this talk on the Coq Github. https://github.com/coq/coq/issues/10871

view this post on Zulip Andrew Ashworth (Oct 10 2019 at 14:57):

The comments are quite interesting to me but I must avoid procrastinating by searching for "subject reduction" and starting down that rabbit hole...

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

They seem to be quite pissed.

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

I just want a prover that is usable for a working mathematician. They admit that Lean's quotient types solve 99% of my problems.

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

After that, they call Lean a "broken system". I don't know what that means.

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

I haven't seen a proof of false yet, in Lean. My Lean doesn't seem very broken.

view this post on Zulip Edward Ayers (Oct 10 2019 at 15:11):

In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all).

What's an example of Lean breaking subject reduction?

view this post on Zulip Rob Lewis (Oct 10 2019 at 15:24):

I think Pierre-Marie has in mind the same issue Mario describes in the last paragraph of 3.1.1. here: https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf

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

I'll freely admit that I don't know a thing about these issues, but is this a problem in practice? As I said, my Lean doesn't seem very broken...

view this post on Zulip Edward Ayers (Oct 10 2019 at 15:45):

I also barely understand this stuff. As far as I can tell, @Mario Carneiro 's §3.1.2 is talking about how you can perform a reduction t ⟿ u such that Lean's typechecker will say that the types are not equal a ⇎ b, but which are actually equal if you added transitivity in a ≡ b. Which doesn't sound that bad. But ppedrot in the issue seems to be talking about subject reduction breaking because of adding in quot.lift f _ (quot.mk a) ~~> f a.

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

A post like this makes me think there are some other reasons why Lean attracts "stupid" mathematicians that don't know a thing about ITPs whereas Coq does not: https://github.com/coq/coq/pull/9381#issuecomment-460077015

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

And the eternal battle for being constructive: https://github.com/coq/coq/pull/9381#discussion_r254167644

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

@Kevin Buzzard That's what you can answer next time someone asks you why Lean owns Coq...

view this post on Zulip Olli (Oct 10 2019 at 17:58):

@Johan Commelin what is the main feature of Lean that makes it less constructive than Coq? I was under the impression that they are mostly the same

view this post on Zulip Mario Carneiro (Oct 10 2019 at 17:58):

Subject reduction breaks in lean, but quotients are not the reason, subsingleton elimination + proof irrelevance is

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

@Olli The community.

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

It's a social thing.

view this post on Zulip Olli (Oct 10 2019 at 18:00):

@Johan Commelin ok, so it's basically the proportion of library work that has gone into the theorems proved using classical logic?

view this post on Zulip Mario Carneiro (Oct 10 2019 at 18:00):

it's an obscure technical issue though, and I hadn't heard that coinductive types break SR in Coq but it sounds similarly irrelevant

view this post on Zulip Floris van Doorn (Oct 10 2019 at 18:00):

I wrote a response, but I'm wondering whether I should post it there. I don't want to cause a flame war. However, I also don't see the email address of Pierre-Marie Pédrot anywhere publicly, so that I can discuss this in private.

Hi, long-term Lean user here. I don't want to start a flame war, but I just want to address @ppedrot's concern about quotients causing a failure of subject reduction.

The reason that quotients cause a failure of subject reduction is a historical design issue with quotients, and not anything that comes up in practice. The problem is the interaction between quotients and definitional proof irrelevance (which Lean has for its bottom universe Prop). The problem is that quotients can be defined for types in all universes, even for propositions. In this case, we can get a failure of subject reduction (described here).

Note that taking a quotient of a proposition is a useless operation, because all propositions are already subsingletons. We only take quotients of types that are not in Prop in practice, and the problem doesn't occur there.

Ideally, we would remove the ability to take quotients of propositions from Lean. This would remove this failure of subject reduction (there is still another failure with inductive families of propositions + proof irrelevance) and would not decrease the usability of quotients.

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

But they shouldn't be surprised that there are no mathematicians knocking on their doors... given what I just read in those threads. That's fine. I respect what they are doing. But they really shouldn't be surprised that mathematicians turn away immediately. It is very very easy to forget that 98% of the mathematicians has NO IDEA what being constructive means.

view this post on Zulip Floris van Doorn (Oct 10 2019 at 18:01):

Johan Commelin what is the main feature of Lean that makes it less constructive than Coq? I was under the impression that they are mostly the same

The fact that we extensively use the axioms we add to Lean (mostly the axiom of choice).

view this post on Zulip Olli (Oct 10 2019 at 18:02):

ok, yeah that was what I thought, and was just curious if there might have been a more technical reason

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

@Olli I'm dead serious. Ask any random mathematician in an actual math department. They don't know what intuitionism is. Beyond maybe some historical anecdote involving Brouwer and Hilbert.

view this post on Zulip Mario Carneiro (Oct 10 2019 at 18:05):

The real reason SR is a bigger deal in coq is because the community does more DTT things, constructive things, etc

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

Thanks for writing that reply. Even if you only share it here... :smiley:

view this post on Zulip Wojciech Nawrocki (Oct 10 2019 at 18:38):

Does Lean obey, vaguely, a sort of weakened form of subject reduction? For example, that one can always exhibit an Id(a,b) if t: a --> u: b.

view this post on Zulip Floris van Doorn (Oct 10 2019 at 18:42):

I sent an email directly to Pierre-Marie Pédrot, I didn't want to start this discussion publicly.

view this post on Zulip Floris van Doorn (Oct 10 2019 at 18:45):

@Wojciech Nawrocki The "weakened" subject reduction is that in Mario's paper satisfies subject reduction. I think this translates to "if t reduces to u, and t : A then you have to apply a finite number of type ascriptions (... : T) to subterms of u and that term will have type A." (EDIT: as Mario pointed out below you need to use @id T ... instead)

view this post on Zulip Wojciech Nawrocki (Oct 10 2019 at 18:49):

Oh, you can actually force the algorithmic equality to recognize every by using type ascriptions?

view this post on Zulip Floris van Doorn (Oct 10 2019 at 18:53):

Oh, you can actually force the algorithmic equality to recognize every by using type ascriptions?

Yes, because the algorithmic equality just fails transitivity. So if you give each intermediate step manually (so that the algorithm doesn't have to apply transitivity itself), then Lean can type-check it. @Mario Carneiro can you confirm?

view this post on Zulip Mario Carneiro (Oct 10 2019 at 21:02):

Unfortunately this doesn't literally work in lean, because the elaborator only uses type ascriptions for elaboration, and does not pass that info along to the kernel. But you can make it work if you use id or show to do the type ascription instead

view this post on Zulip Floris van Doorn (Oct 10 2019 at 21:04):

Oh yes, that was the difference between @id T _ and (_ : T).

view this post on Zulip Mario Carneiro (Oct 10 2019 at 21:04):

Assuming there was a way to "hint" intermediate terms to the type checker, yes that's the theorem

view this post on Zulip Miguel Raz Guzmán Macedo (Oct 10 2019 at 23:34):

Olli The community.

FYI I came here this morning because of Kevin's talk at Microsoft from another very welcome open source community and seeing that comment from the Coq devs and this chat's reaction to it has convinced me Lean is the way to go. #OpenAllTheGates

view this post on Zulip Kevin Buzzard (Oct 10 2019 at 23:47):

I'm just catching up with all this after a gruelling day at work. Oh dear. I don't want to annoy people, I just want Lean to get noticed by mathematicians.

view this post on Zulip Miguel Raz Guzmán Macedo (Oct 10 2019 at 23:50):

I'm just catching up with all this after a gruelling day at work. Oh dear. I don't want to annoy people, I just want

Awesome talk by the way!
Is there any place where if we're interested in special functions, algorithms, or
differential equations we can help prove some stuff in lean? or has that work mostly been taken over?

view this post on Zulip Andrew Ashworth (Oct 10 2019 at 23:51):

Oof. There's a million and one things that need to be added to the library. I do not think there will be a lack of work, ever.

view this post on Zulip Andrew Ashworth (Oct 10 2019 at 23:52):

Perhaps just browse Mathlib, see if something you are interested in is there, and if it isn't, try formalizing it

view this post on Zulip Leonardo de Moura (Oct 11 2019 at 02:51):

I'm just catching up with all this after a gruelling day at work. Oh dear. I don't want to annoy people, I just want Lean to get noticed by mathematicians.

@Kevin Buzzard Your talk was fantastic! It is still generating many interesting discussions at MSR. Your talk has more views in one week than any other MSR talk in the last 12 months. You beat even Bill Gates's interview with our director. :big_smile: I have already lost count on how many people stopped in corridors or sent me messages saying they absolutely loved your talk. Well done!


Last updated: May 13 2021 at 06:15 UTC