undefined | Better HN

0 pointsdeadbeef574y ago0 comments

> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.

This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrating way, and frankly I'm a bit sick of it.

Working mathematicians are usually not experts of type theory. Yes. But they aren't stupid either. Why does the Lean community have such a large number of mathematician users? Why did it successfully formalize the main technical result of Peter Scholze's challenge in less than 6 months? Is this all because of a "mastermind PR campaign" selling mathematicians snake oil?

There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.

I'm fine with people finding the foundations of Lean ugly, distasteful, improper, or whatever. But please stop the insults.

0 comments

ImprobableTruth4y ago

The context of that "mastermind PR campaign" comment is a video watched now more than 70,000 times in which it's claimed that Coq is just not as good as Lean because it doesn't have quotient types, even though you can get them if you're willing to make the same trade-off that Lean does (broken SR). Calling Lean's framing a 'mastermind PR campaign' is of course still quite snippy, but I don't think it's totally unfair seeing as how it led to those comments.

>There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.

I think it just takes time to fully move on. And while it's not the fault of the Lean community, when something like the recent quantamagazine article on formalizing mathematics essentially only mentions Coq to call it old and busted in comparison to Lean, that's only going to cause people to hold onto their resentments for longer.

zozbot2344y ago

The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating.

It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.

deadbeef57OP4y ago

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

zozbot2344y ago

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out.

And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

deadbeef57OP4y ago

I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical.

It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)

foooobar4y ago

I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.

Someody424y ago

You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think

1 more reply

j / k navigate · click thread line to collapse

0 comments

ImprobableTruth4y ago

>There has been some strong disagreements and even mud slinging between the Coq and Lean communities in the past. But I thought that axe was buried. I would like to move on.

zozbot2344y ago

deadbeef57OP4y ago

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

zozbot2344y ago

deadbeef57OP4y ago

I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical.

It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)

foooobar4y ago

Someody424y ago

1 more reply

j / k navigate · click thread line to collapse