StackExchange proposed site ProofAssistants

101 views
Skip to first unread message

EricGT

unread,
Nov 25, 2021, 1:56:49 PM11/25/21
to Metamath
This is my first time posting here so please excuse me if this is out of place.

This group was mentioned on another Proof Assistant site asking if this notification was posted at MetaMath. I do not see one.

 Andrej Bauer has proposed the StackExchange site ProofAssistants

The proposal is still open to those wanting to commit before the private beta.

A StackExchange chat room for the ProofAssistants proposal has been setup: https://chat.stackexchange.com/rooms/131732/proofassistants-temp

Jim Kingdon

unread,
Nov 25, 2021, 11:24:53 PM11/25/21
to meta...@googlegroups.com

On 11/25/21 10:17 AM, EricGT wrote:

 Andrej Bauer has proposed the StackExchange site ProofAssistants.

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).


Mario Carneiro

unread,
Nov 26, 2021, 5:50:52 AM11/26/21
to metamath
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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6fe2a7f4-cfdc-c075-4999-ea92ae9a7e01%40panix.com.

EricGT

unread,
Nov 26, 2021, 5:54:54 AM11/26/21
to meta...@googlegroups.com
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)

>  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 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 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.

Andrej Bauer is also on Twitter where many first learned of the proposal.

Regards,
Eric





On Thu, Nov 25, 2021 at 11:24 PM Jim Kingdon <kin...@panix.com> wrote:
--
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 metamath+u...@googlegroups.com.

EricGT

unread,
Dec 9, 2021, 7:18:17 AM12/9/21
to meta...@googlegroups.com
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.

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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsjiEbP8%3DwMB32a_S6WJExHctDKuG-%2BRucosSOjNO0k5A%40mail.gmail.com.

EricGT

unread,
Feb 13, 2022, 7:43:08 AMFeb 13
to meta...@googlegroups.com
FYI

The site StackExchange Proof Assistants site went live last Tuesday

Here are some stats. 

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.
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






Reply all
Reply to author
Forward
0 new messages