Article says: > 1. There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and m

Article says: > 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? I think many of the formal proof verification communities are trying to address these. I will focus on Metamath, especially its set.mm database that focuses on classical logic + ZFC ( http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html ), but much of the following applies to all of them. I think the main problem is that too many mathematicians expect computer systems to have all the capabilities of a well-trained graduate mathematician. Yet the problem is hard. Computers are much better at some things (they don't get bored or sleepy), and humans are much better at other things (seeing the big picture & having insights into how to combine "unrelated" ideas). Much would be better if the formalization and traditional mathematics communities had more "meetings of the minds" & communication in general. Focusing on these questions: 1. The high learning curve is true for all systems, that's true. To be fair, mathematics has a high learning curve, you don't learn how to do it in a week. The problem is that although tools are very good at verifying formalized proofs, they are not great at coming up with the proofs themselves. I do agree that the documentation could be improved so "non computer scientists" could do things more easily. I think much of what's needed is for traditional mathematicians to engage with the formalization community, to make it clearer what's missing. There also needs to be work (and funding) on improved tooling, which implies a need for more funding (I'll discuss that below). 2. "They will not find much fashionable mathematics." There's a chicken-and-egg problem here. It takes a while to get proofs up to the "basics" of mathematics as expected by people work on "fashionable" mathematics. Here I think the solution is to have many people working to build up those basics. Take a look at my visualization of Metamath set.mm; note that it took many years for it to build up, and only when many people joined did it start seriously growing: https://www.youtube.com/watch?v=XC1g8FmFcUU https://www.youtube.com/watch?v=XC1g8FmFcUU The real bottom line is that there really needs to be more funding on tools & formalized systems. Metamath isn't funded at all to my knowledge. Lean and Coq have some funding, but nothing like the funding of many other fields. We should be impressed about how far they've come in spite of that. A broader problem is that mathematicians typically accept a proof if a paper seems to be okay to another mathematician. When the math and proofs were simpler, that was probably fine, and since computers weren't very capable that's all we could do anyway. But today's math (and proofs) are far more complex, and it's becoming absurd to leave that as our standard of proof. Computers are available now; we should be using them.