[FOM] Improving Set Theory

[Timothy Y. Chow]

On Wed, 15 Jan 2020, Emilio Jesús Gallego Arias wrote:
>>> Lean does not have this problem. For me, Lean is the only one worth 
>>> learning if you actually want to do mathematics.
>
> As already pointed out by other people this seems like a pretty bold 
> claim given that people has been successfully doing pretty advanced 
> maths in Coq, Isabelle, HOL, Mizar, etc... for a quite a bit of time.

Buzzard is certainly capable of defending himself, but I do want to make a 
remark here.  Many mathematicians have what I regard as an unfortunate 
tendency to use the word "mathematics" to refer only to the type of math 
they do research in.  I noticed Voevodsky doing this, and I think that 
Buzzard is somewhat guilty of it here.  If one is charitable then I think 
that where Buzzard says "actually want to do mathematics," one should read 
"mathematics" as "modern number theory."  Modern number theory has perhaps 
more than its fair share of ineffective results.  Also, some of the 
abstractions that one wants to define---say, group schemes or stacks or 
perfectoid spaces or topoi---require somewhat more piling of definitions 
on top of other definitions than in many other branches of mathematics. 
So a framework that works tolerably well in other contexts might show 
signs of strain here.

Again, I'm not necessarily trying to argue that Buzzard is correct, since 
I don't have enough first-hand knowledge of either Coq or Lean to have my 
own opinion, but I think this may help set his comments in context.

Tim