It is a great call to arms (both the original blog post, and your response, David).
I don't think I have a lot of suggestions other than "keep formalizing things, building up as many fields of mathematics as we can". Well, and working to improve tools and all the other things we do. There is a large amount of critical mass involved in making these tools (and their proof databases) big enough and capable enough to "do mathematics" in a fuller sense. With each proof or tool improvement we get one step closer, and I like to think that my own efforts have their small contribution to make in bridging the gap between the world of constructive mathematics (which often uses type theory) and textbook understanding (which most often is set theory with excluded middle). But it is just one piece in a very large world. As for communication tools and whether mailing lists are too old school, I hope we've made one step forward by getting on github (at least, speaking for myself I'm not sure I would have made it over the hump of becoming a contributor without github). If I set up a Slack workspace, would anyone join it? (Slack is a chat room platform often used within companies but also sometimes in community contexts, with a decent free tier). Or perhaps there already is a slack workspace for math stuff and I just don't know about it? On February 22, 2020 1:02:12 PM PST, "David A. Wheeler" <[email protected]> wrote: >Fyi, There is an interesting essay about math formulas ation here: >https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ > >There is a discussion about it here: >https://news.ycombinator.com/item?id=22390486 >--- David A.Wheeler > >-- >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/75C0C03C-88A9-44FC-9C36-EA466B90053E%40dwheeler.com. -- 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/5489D299-C6C9-400A-B29B-18D0CCA47022%40panix.com.
