## Stream: general

### Topic: Kevin's talk at MSR

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

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

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

#### Johan Commelin (Oct 10 2019 at 15:02):

They seem to be quite pissed.

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

#### Johan Commelin (Oct 10 2019 at 15:03):

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

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

#### 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?

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

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

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

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

#### Johan Commelin (Oct 10 2019 at 16:35):

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

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

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

#### Mario Carneiro (Oct 10 2019 at 17:58):

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

#### Johan Commelin (Oct 10 2019 at 17:59):

@Olli The community.

#### Johan Commelin (Oct 10 2019 at 17:59):

It's a social thing.

#### 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?

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

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

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

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

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

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

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

#### Johan Commelin (Oct 10 2019 at 18:31):

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

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

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

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

#### Wojciech Nawrocki (Oct 10 2019 at 18:49):

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

#### 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?

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

#### Floris van Doorn (Oct 10 2019 at 21:04):

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

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

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

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

#### 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?

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

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

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