FYI The site StackExchange Proof Assistants site went live last Tuesday https://proofassistants.stackexchange.com/
Here are some stats. https://area51.stackexchange.com/proposals/126242 Metamath is getting lots of mentions and good press. I am happy to see it noted in questions and answers. Currently the site is in private beta which years ago meant that you could only get access by committing earlier and then receiving an invite via email. However I have heard that may have changed and just visiting site and logging in are all that are needed. https://proofassistants.stackexchange.com/ If you did commit you should have received the invite email with the link. I did receive one so I can confirm this. Regards, Eric https://stackexchange.com/users/1291795/guy-coder On Thu, Dec 9, 2021 at 7:18 AM EricGT <[email protected]> wrote: > Proof Assistants private beta launch will take place in January 2022 > <https://area51.meta.stackexchange.com/questions/32670/proof-assistants-private-beta-launch-will-take-place-in-january-2022> > > > Since we want all proposals to have the best chances of thriving as > possible, the Community Team has decided to postpone this proposal's launch > into private beta to January 2022, in an attempt to minimize the impact of > the upcoming end-of-year holidays in the site's chances of success. > > > > Additionally, the proposal sped through its definition and commitment > phases, which we believe hasn't allowed for some discussions that usually > take place during those phases — such as deciding on a name and URL for the > site — to come to a consensus. As such, we invite those of you who've > committed to this proposal to try to have those conversations between now > and the first couple of weeks of January 2022. At that time the Community > Team will help y'all tie whatever loose ends need to be tied, and prepare > the site for launch into private beta. > > On Fri, Nov 26, 2021 at 5:50 AM Mario Carneiro <[email protected]> wrote: > >> 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 a topic in the >> Google Groups "Metamath" group. >> To unsubscribe from this topic, visit >> https://groups.google.com/d/topic/metamath/CsUtKJPdI_s/unsubscribe. >> To unsubscribe from this group and all its topics, 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 >> <https://groups.google.com/d/msgid/metamath/CAFXXJSsjiEbP8%3DwMB32a_S6WJExHctDKuG-%2BRucosSOjNO0k5A%40mail.gmail.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/CAN45N11PSAgTYhNh_tK94XXy27u4ZtyN8gV-j1Pz0C%3DEho7efw%40mail.gmail.com.
