Perhaps somewhat off-topic, but Zulip seems to already be a tool of choice, is the primary chat space for both Lean and Coq. We have one set up for xi and druid (xi.zulipchat.com) I find it very good. It's open to all with a github account, and we haven't had a single case of a spammy or abusive signup, out of 932 so far.
It is free for open source projects, and I'm happy to put in a word of recommendation. (I loosely know the developers) Btw Kevin's impassioned rant is also very interesting. I seriously wonder whether dependent type theory is the best foundation for "real mathematics" though strongly appreciate the lure of it. Some of the discussion on HN is interesting but it seemed to go off the rails thanks to one "designated asshole" - what do presidential election choices and amphetamines have to do with the topic of making formalized mathematics accessible to larger groups of mathematicians? Raph On Sat, Feb 22, 2020 at 7:10 PM Jim Kingdon <[email protected]> wrote: > 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/5489D299-C6C9-400A-B29B-18D0CCA47022%40panix.com > <https://groups.google.com/d/msgid/metamath/5489D299-C6C9-400A-B29B-18D0CCA47022%40panix.com?utm_medium=email&utm_source=footer> > . > -- 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/CADBEgNM5iHTwQxqu6wmhcFiXm8Q6rg98-Q_DF8ZfKiYmGg%3Dz%2Bg%40mail.gmail.com.
