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.
