Further to that, there are large ongoing efforts in formalizing mathematics on computers now. https://news.ycombinator.com/item?id=25118372 https://news.ycombi

Further to that, there are large ongoing efforts in formalizing mathematics on computers now. https://news.ycombinator.com/item?id=25118372 https://news.ycombinator.com/item?id=25118372 Several of them are getting pretty far, and none of them are directly using PM notation (although all of them ultimately owe something to PM). You can learn more math, or contribute more to math, nowadays by learning one or more of these systems. To my knowledge, all of them are eager for new volunteers to continue formalizing theorems in their respective databases.