Oh word
Quote Tweet
Why do proof assistants use dependent type theory instead of set theory? mathoverflow.net/questions/3768
1
13
Conversation
The idea of Lean working for all of math is absurd though, . You are very quotable, but come on, that is sensationalist, the assumption of UIP alone rules out many kinds of mathematics.
3
9
Hi Talia! I think you're completely wrong on this. I think that people who don't work in maths departments often have a view of mathematics which is quite detached from what is *actually happening in maths departments*. I don't see any reason why UIP stops me formalising maths.
2
1
It doesn't stop you, but it is one choice in a fork where univalence works just as nicely (in fact gives rise to the automation you like more easily). And it stops folks working in proof relevant mathematics; "all of math" is just a hyperbolic statement.
1
1
I was a math researcher before I went into CS, by the way. I didn't start programming until college.
It is important to be nuanced in these conversations or you lose the important lessons of why Lean has been useful for you. Foundations are not why.
1
4
My understanding is two things about Lean have helped you a lot: good automation and good library support. The latter of which has been a lot of your effort.
Other proof assistant designers should learn from this. Losing this nuance in discussion is a major loss for everyone
2
4
Not sure if this is part of 'good automation', or if it's more just 'tooling', but as a non-expert on theorem proving, I've appreciated Lean because it makes it easy to set up VS Code with live-updating intellisense.
1
I think the Agda and Coq folks are working on trying to improve support for these kinds of editors, but it seems like a big undertaking. It does help to reduce the barrier to entry to not have to go through emacs though.
1
Too the point at hand, this is all orthogonal to foundations. More about how easy it is to get up and running, and start doing meaningful stuff. I'm sure the way Lean does tactics helps ease that even more (seeing as they are written in Lean itself).
Really would prefer to use a language with foundations set up for cubical stuff though, so I'm hoping other languages can learn from this lesson! 😅
1
I would love to see any development of basic algebraic geometry (affine schemes as topological spaces+sheaf of rings) in a univalent setting. Voevodsky never managed to achieve this, and people have told me that he wasn't trying to do it; I would have loved to ask him why not 😐
1