I am also pretty supportive of the new site. The lean zulip basically flash mobbed the site proposal page and pushed it to "committed" status in record time (it often takes months, but here it reached critical mass in a single weekend). The Coq zulip also seems interested in participating, and Isabelle might also join in although the leadership there is very anti-corporatism so they might just stick to what they are doing.
As for metamath, it's definitely nice to have a place to post Q/A questions about metamath without them being off topic and unlikely to reach anyone. But a lot of the prover communities are concerned about splitting discussion between the stack exchange and the mailing list / chat room / forum that they have been using until now, and metamath has a similar issue (when should you use the google group vs the stack exchange?). My guess is that it won't be too successful, but I'm signed up for the new site and we'll see how it goes. Mario Carneiro On Thu, Nov 25, 2021 at 11:24 PM Jim Kingdon <[email protected]> wrote: > On 11/25/21 10:17 AM, EricGT wrote: > > Andrej Bauer has proposed the StackExchange site ProofAssistants > <https://area51.stackexchange.com/proposals/126242/proof-assistants?referrer=NTIzNzFkNWM5ZDZlZjU5Mzk3NWY2MDM1YWI5OGZlMzUzZGRlNWQxNzU5YzYzYTEwMjY4OTJiY2MyNDRjYTNhYuaBr5YwQ5SZ2E_DDdrudzEHUMW1pi7ReJnaMg8cuFSp0>. > > > Thanks for posting this. I don't do enough with StackExchange to fully > understand the process of making a site, but this sounds cool and as I > understand it, metamath would be on-topic there. > > For those who don't know Andrej Bauer, several of his papers are cited in > the iset.mm bibliography including a delightful introduction to > constructive mathematics and a rather detailed paper on how to construct > the real numbers without excluded middle. > > I also saw at least one other familiar name (Mike Shulman, who reviewed my > pull requests for small wording tweaks to the HoTT book). > > > -- > 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/6fe2a7f4-cfdc-c075-4999-ea92ae9a7e01%40panix.com > <https://groups.google.com/d/msgid/metamath/6fe2a7f4-cfdc-c075-4999-ea92ae9a7e01%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/CAFXXJSsjiEbP8%3DwMB32a_S6WJExHctDKuG-%2BRucosSOjNO0k5A%40mail.gmail.com.
