The reason I posted the notice for those on MetaMath is that that Jason Rute asked if MetaMath was notified. I did not see a notice here. (ref <https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/A.20proposal.20for.20StackExchange.20.22Proof.20assistants.22.20site/near/262183144> )
> 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. Yes metamath would be on topic there. Don't worry about not understanding the process of making a site, this FAQ <https://area51.stackexchange.com/faq>gives the high level overview. The next step for the site is to enter the private beta which is expected to be on a Tuesday either Dec 7th or Dec 14th. The private beta is expected to last about 3 weeks. If users of MetaMath commit <https://area51.stackexchange.com/proposals/126242?phase=commitment>to participate in the private beta that would be helpful but *not necessary*. Once the site goes into public beta anyone can join and just observe if desired. If one has questions please ask and I will try to answer them. There is also a public chat room on StackExchange for the proposed site while the servers and such are being set up. https://chat.stackexchange.com/rooms/131732/proofassistants-temp Andrej Bauer is also on Twitter where many first learned of the proposal. https://twitter.com/andrejbauer Regards, Eric 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 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/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/CAN45N13_oC-4fkfQimSgev%2BHzELGR_3Y4tQWyO1oRW5SmVL4Kw%40mail.gmail.com.
