Timeline for What makes dependent type theory more suitable than set theory for proof assistants?
Current License: CC BY-SA 4.0
31 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 28, 2023 at 20:12 | comment | added | Stefan | I'm surprised all the answers focus basically on the typed/untyped difference. Does the fact that propositions&proofs are themselves naturally first class objects in type theory matter in practice? What about the layering needed to avoid impredicative paradoxes? | |
| Nov 22, 2020 at 17:15 | comment | added | Kevin Buzzard | @DavidCorfield Yes, I guess if you learn to use a prover, and you want a PhD thesis/some papers, then the thing to do is to work on the area where the prover is doing well. What exasperates me about this whole ecosystem is that whilst I believe it can revolutionise mathematics-as-I-understand-it, there seems to be no drive from within the area to attract mathematicians-as-I-understand-them. My talk is specifically about mathematics-as-I-understand-it in a theorem prover and, for that, most of the systems are worse than useless because they haven't focussed on it so little is done. | |
| Nov 22, 2020 at 12:28 | comment | added | YCor | The first questionable assertion sounds, in my opinion, unnecessary to motivate the question and uselessly aggressive (and the author seems to regret this quote). I'd suggest to replace it with something akin to "In his talk [link], KB emphasizes that type theory is the only way to formalize all of math. In the Q&A..." | |
| Nov 21, 2020 at 11:09 | comment | added | MWB | @none That example is not very good IMHO. Those existentially quantified variables could simply be replaced by Skolem functions of the variables that they actually depend on. | |
| Nov 21, 2020 at 9:12 | comment | added | none | Terry Tao in this 2007 blog post gives an example of a straightforward mathematical statement that he says appears impossible to express in first order set theory. The post's comment section has some additional discussion of how it can be dealt with. | |
| Nov 20, 2020 at 22:20 | vote | accept | MWB | ||
| Nov 20, 2020 at 22:18 | comment | added | Mike Shulman | @KevinBuzzard In addition to David and Christopher's points, which are largely correct, many people working on HoTT/UF are just not interested in simply formalizing known facts but are more interested in pushing the boundaries. Also there are a lot fewer of us than there are people working in ordinary Coq, and furthermore UniMath is just one project while others like HoTT/HoTT have no objection to using all the features of Coq. | |
| Nov 20, 2020 at 20:31 | answer | added | Joe Hendrix | timeline score: 8 | |
| Nov 20, 2020 at 17:19 | comment | added | Christopher Hughes | I might be wrong, but I think a lot of the maths implemented in Coq, e.g. Odd Order Theorem are done in a logic weaker than HoTT, so in some sense a bunch of maths has been formalised in HoTT, they just never actually used the univalence axiom. | |
| Nov 20, 2020 at 15:56 | comment | added | David Corfield | @KevinBuzzard Perhaps worth repeating here the response of some UniMath people that as many are postdocs looking for permanent positions, this won't happen if all they are seen to have achieved is the reproduction of textbook mathematical proofs. | |
| Nov 20, 2020 at 15:32 | comment | added | Kevin Buzzard | Yes, this summarises it well! I have given 20+ talks on this stuff now, and some get recorded, but somehow this one talk went crazy and I completely inadvertantly upset a bunch of Coq users. I do have strong opinions about what is good and bad about the Coq ecosystem but I do a poor job of summarising them in the talk. I have posted far more well-thought-out comments elsewhere (e.g. on the Coq Zulip) but nothing gets the traction of this talk. | |
| Nov 20, 2020 at 14:55 | comment | added | Yemon Choi | @KevinBuzzard I am reminded of the following bit from one of Terry Pratchett's books: "In my experience, Miss Cripslock tends to write down exactly what one says ... It's a terrible thing when journalists do that. It spoils the fun. One feels instinctively that it's cheating, somehow." :) | |
| Nov 20, 2020 at 14:30 | comment | added | Kevin Buzzard | @ToddTrimble -- I don't know what I said, but here's what I meant: Coq itself has got a huge bunch of mathematics, including as you say Feit-Thompson. But Voevodsky's UniMath project, which is built on Coq but is not the same as Coq because it contains rules such as "there are certain things which you can do in Coq but you're not allowed to do in UniMath", has very little of the mathematics that one would see in a typical undergraduate degree | |
| Nov 20, 2020 at 13:59 | answer | added | Kevin Buzzard | timeline score: 33 | |
| Nov 20, 2020 at 13:50 | comment | added | Kevin Buzzard | Let me state, once again, that I thoroughly regret bad-mouthing Coq in a talk which I had no idea would go "viral" to the extent that it has. | |
| Nov 20, 2020 at 12:57 | history | became hot network question | |||
| Nov 20, 2020 at 12:02 | answer | added | Andrej Bauer | timeline score: 233 | |
| Nov 20, 2020 at 5:20 | comment | added | Todd Trimble | @TimothyChow Thanks; I listened again and you're right. Still, I'm not sure how to take this assertion of "doing nothing". | |
| Nov 20, 2020 at 4:06 | comment | added | Timothy Chow | @ToddTrimble : I think that what Buzzard said is that in 15 years, the univalent foundations people have done "nothing," in contrast to "15 years in Coq, they were really doing stuff." Start listening at 1:02:16 and slow it down to 0.5 speed. | |
| Nov 20, 2020 at 2:29 | comment | added | Todd Trimble | I hope Buzzard joins the discussion. But one thing I found strange is this mention of "chaps" around Voevodsky who haven't done anything with Coq except formalize rings and modules. Did I hear that correctly? It sounded really misleading. Clearly there are extensive libraries of math formalized by Coq; for example, the formalization of the odd order theorem (finite groups of odd order are solvable) by Gonthier et al. was one such tour de force, although not necessarily one developed by the "Voevodsky chaps". | |
| Nov 20, 2020 at 2:04 | answer | added | Mozibur Ullah | timeline score: 1 | |
| Nov 19, 2020 at 18:49 | answer | added | Timothy Chow | timeline score: 44 | |
| Nov 19, 2020 at 17:58 | history | edited | LSpice | CC BY-SA 4.0 |
Inlined Youtube link, and linked to particular time
|
| Nov 19, 2020 at 17:43 | history | edited | MWB | CC BY-SA 4.0 |
added 57 characters in body
|
| Nov 19, 2020 at 17:30 | comment | added | MWB | @AsafKaragila I believe he said he'd started with Coq and switched to Lean after 2 weeks. | |
| Nov 19, 2020 at 17:18 | comment | added | Asaf Karagila♦ | @YCor: People who are trying to push their agenda, will usually try to minimise other things. At least "in broad strokes" parts of their agenda... (I'm not accusing Kevin of being unethical, I'm just offering an explanation: if you want people to use Lean and follow your philosophical agenda, it's usually counterproductive to say "Actually set theory is great and you should study it, or at least use Coq for a year or two, before coming to use Lean"...) | |
| Nov 19, 2020 at 17:14 | comment | added | MWB | @YCor he mentions Coq a few times. | |
| Nov 19, 2020 at 17:13 | comment | added | YCor | It's also tempting to ask about accuracy of the sentence that it's the only existing such proof assistant which suggests that other proof assistants such as Coq are not "suitable for formalizing all of math". | |
| S Nov 19, 2020 at 17:01 | history | suggested | jeq | CC BY-SA 4.0 |
Typo in title.
|
| Nov 19, 2020 at 16:08 | review | Suggested edits | |||
| S Nov 19, 2020 at 17:01 | |||||
| Nov 19, 2020 at 4:59 | history | asked | MWB | CC BY-SA 4.0 |