Kevin's talk at MSR

Stream: general

[Leonardo de Moura]

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

[Daniel Selsam]

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

[Reid Barton]

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.

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Johan Commelin]

They seem to be quite pissed.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Edward Ayers]

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?

[Rob Lewis]

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

[Johan Commelin]

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...

[Edward Ayers]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Olli]

@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

[Mario Carneiro]

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

[Johan Commelin]

@Olli The community.

[Johan Commelin]

It's a social thing.

[Olli]

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

[Mario Carneiro]

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

[Floris van Doorn]

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.

[Johan Commelin]

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.

[Floris van Doorn]

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).

[Olli]

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

[Johan Commelin]

@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.

[Mario Carneiro]

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

[Johan Commelin]

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

[Wojciech Nawrocki]

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.

[Floris van Doorn]

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

[Floris van Doorn]

@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)

[Wojciech Nawrocki]

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

[Floris van Doorn]

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?

[Mario Carneiro]

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

[Floris van Doorn]

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

[Mario Carneiro]

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

[Miguel Raz Guzmán Macedo]

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

[Kevin Buzzard]

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.

[Miguel Raz Guzmán Macedo]

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?

[Andrew Ashworth]

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.

[Andrew Ashworth]

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

[Leonardo de Moura]

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!