>My favorite is around 1:04:00 when someone asks a second time why he disprefers coq, and Buzzard complains that it can't represent some advanced quotient type that he'd have to work around. I'm reminded of [1]
Second what abstractcontrol said.[0] I wouldn't say being able to deal with quotient types is a "trivial" feature, because Buzzard does explain his reason for why quotient types are crucial for what he does.
The motivation is that he wants to formalise a concept that is the subject of current active research, instead of yet another concept from undergraduate mathematics. In this case, it's the notion of perfectoid spaces,[1] which was only introduced in 2012 by Peter Scholze.[2]
The justification for this is sociological: research mathematicians predominantly find the retreading of old ground boring and trivial. Buzzard wants to sell the power of theorem provers to exactly these mathematicians, so he felt that formalising something that many number theorists would be intensely interested in may have more impact.
Unfortunately, while I'd like to think that he's succeeded somewhat, the reaction I've seen is just more of the "well, isn't that nice" variety, outside of some enthusiasts, many of whom are young and/or not very influential. Mainly, it's because theorem provers still can't help mathematicians improve their productivity, because there's still a lot of stuff that's still missing in the ecosystem, and Buzzard pointed out some of the missing "features" that may help theorem provers take off.
>[1] https://prog21.dadgum.com/160.html Dangling by a trivial feature
Second what abstractcontrol said.[0] I wouldn't say being able to deal with quotient types is a "trivial" feature, because Buzzard does explain his reason for why quotient types are crucial for what he does.
The motivation is that he wants to formalise a concept that is the subject of current active research, instead of yet another concept from undergraduate mathematics. In this case, it's the notion of perfectoid spaces,[1] which was only introduced in 2012 by Peter Scholze.[2]
The justification for this is sociological: research mathematicians predominantly find the retreading of old ground boring and trivial. Buzzard wants to sell the power of theorem provers to exactly these mathematicians, so he felt that formalising something that many number theorists would be intensely interested in may have more impact.
Unfortunately, while I'd like to think that he's succeeded somewhat, the reaction I've seen is just more of the "well, isn't that nice" variety, outside of some enthusiasts, many of whom are young and/or not very influential. Mainly, it's because theorem provers still can't help mathematicians improve their productivity, because there's still a lot of stuff that's still missing in the ecosystem, and Buzzard pointed out some of the missing "features" that may help theorem provers take off.
[0] https://news.ycombinator.com/item?id=21239067
[1] https://en.wikipedia.org/wiki/Perfectoid_space
[2] https://en.wikipedia.org/wiki/Peter_Scholze