StackExchange proposed site ProofAssistants
111 views
Skip to first unread message
EricGT
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.
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
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
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
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.--
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
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)
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.
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
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.
> 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
Feb 13, 2022, 7:43:08 AM2/13/22
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