He is trying to deliver this message to all, so I think people here might be interested too:
Each formal proof verification system (Lean, Coq, Isabelle/HOL, UniMath, > all of the others) has its own community, and it is surely in the interests > of their members to see their communities grow. These systems are all > *claiming > to do mathematics*, as well as other things too (program verification, > research into higher topos theory and higher type theory etc). But two > things have become clear to me over the last two years or so: > > 1. There is a large community of mathematicians out there who simply > cannot join these communities because the learning curve is too high and > much of the documentation is written for computer scientists. > 2. Even if a mathematician battles their way into one of these > communities, there is a risk that they will not find the kind of > mathematics which they are being taught, or teaching, in their own > department, and there is a very big risk that they will not find much > fashionable mathematics. > > My *explicit question* to all the people in these formal proof > verification communities is: what are you doing about this? > Full post is here: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6478d27f-2d3b-4296-9f95-9236562bd7e8%40googlegroups.com.
