Metamath website - current status
80 views
Skip to first unread message
David A. Wheeler
Mar 1, 2023, 9:22:30 PM3/1/23
to Metamath Mailing List
All, FYI, here's the current status of the main Metamath website metamath.org & us.metamath.org.
First: a few days ago I finally got the metamath.org DNS registration officially transferred from Norman Megill to me. My thanks to his partner, Susan Cass, who helped me work through the process. Norm & I had talked about what would happen when he died, and we had *started* to prepare for that eventuality. However, we had expected that he had much more time than he did, so we weren't fully prepared. I miss him, as I know many of you do. That said, we're moving forward. I've put Susan Cass on the "bcc:" of this message, because I want her to know that we are working to keep Norm's passion project moving forward.
Since that DNS transition is official, I thought now would be a good time to tell everyone the current state of the metamath.org website. In short: everything seems to be working & under control. Here are the key points:
* I have control over the DNS name metamath.org. Should I unexpectedly die (and that's not my preference), I intend for Mario Carneiro to immediately take over. Registration is currently with domainmonger & automatically renews. Fees aren't due until 2030, and the current price there is $18/year. Its configuration redirects requests of "metamath.org" to <https://us.metamath.org/mm.html>.
* The website itself is running on linode. Up to this point that's cost me $5/month, but they've just been bought out, and I was informed today that they're adding 20% to their fee on April 1. So it'll be $6/month ($72/year). At the moment I plan to just leave it on linode (as it takes effort to move), but I want to ensure we *can* move. As you know, the website has https:// (TLS) running, has various security countermeasures enabled (such as package auto-updates & HTTPS headers), and updates the proofs & such daily. The update scripts are horrendously messy, but they work & the plan is to clean them up over time. More generally, my intent is to enable people to continuously improve things.
If you're in good financial shape & want to chip in to help fund it, send me an email; I'll send my home address & you can send me a check. However, do *NOT* feel obligated to send any money, especially if you are (for example) a recently-minted PhD in mathematics who is working for a university :-). While I'm not made of money, that's not much money, and many of you have incredible gifts in mathematics & related fields. I'd rather people spent their resources on other stuff like new/improved proofs, improved tools, and better documentation. I can afford a few dollars to keep a website up, and improvements in those areas are more important to me.
In the longer term I'd like to create a nonprofit association to manage these things. The goal would be to set up something that could outlive us all. Its notional purpose would be something like "Enable and encourage computer-verified formalization of mathematics.". The association would control the domain name, GitHub account, and so on, and would have board members & such to make decisions. Setting up an association takes time & money, though, so I haven't done anything serious about it yet. For the moment, the key is to keep improving so that there's something worth creating an association for.
My thanks to everyone who's ever contributed in any way. You are appreciated.
--- David A. Wheeler
First: a few days ago I finally got the metamath.org DNS registration officially transferred from Norman Megill to me. My thanks to his partner, Susan Cass, who helped me work through the process. Norm & I had talked about what would happen when he died, and we had *started* to prepare for that eventuality. However, we had expected that he had much more time than he did, so we weren't fully prepared. I miss him, as I know many of you do. That said, we're moving forward. I've put Susan Cass on the "bcc:" of this message, because I want her to know that we are working to keep Norm's passion project moving forward.
Since that DNS transition is official, I thought now would be a good time to tell everyone the current state of the metamath.org website. In short: everything seems to be working & under control. Here are the key points:
* I have control over the DNS name metamath.org. Should I unexpectedly die (and that's not my preference), I intend for Mario Carneiro to immediately take over. Registration is currently with domainmonger & automatically renews. Fees aren't due until 2030, and the current price there is $18/year. Its configuration redirects requests of "metamath.org" to <https://us.metamath.org/mm.html>.
* The website itself is running on linode. Up to this point that's cost me $5/month, but they've just been bought out, and I was informed today that they're adding 20% to their fee on April 1. So it'll be $6/month ($72/year). At the moment I plan to just leave it on linode (as it takes effort to move), but I want to ensure we *can* move. As you know, the website has https:// (TLS) running, has various security countermeasures enabled (such as package auto-updates & HTTPS headers), and updates the proofs & such daily. The update scripts are horrendously messy, but they work & the plan is to clean them up over time. More generally, my intent is to enable people to continuously improve things.
If you're in good financial shape & want to chip in to help fund it, send me an email; I'll send my home address & you can send me a check. However, do *NOT* feel obligated to send any money, especially if you are (for example) a recently-minted PhD in mathematics who is working for a university :-). While I'm not made of money, that's not much money, and many of you have incredible gifts in mathematics & related fields. I'd rather people spent their resources on other stuff like new/improved proofs, improved tools, and better documentation. I can afford a few dollars to keep a website up, and improvements in those areas are more important to me.
In the longer term I'd like to create a nonprofit association to manage these things. The goal would be to set up something that could outlive us all. Its notional purpose would be something like "Enable and encourage computer-verified formalization of mathematics.". The association would control the domain name, GitHub account, and so on, and would have board members & such to make decisions. Setting up an association takes time & money, though, so I haven't done anything serious about it yet. For the moment, the key is to keep improving so that there's something worth creating an association for.
My thanks to everyone who's ever contributed in any way. You are appreciated.
--- David A. Wheeler
Glauco
Mar 2, 2023, 5:37:18 PM3/2/23
to Metamath
Thank you, David
without your dedication, it would be really hard to keep the Metamath ecosystem well organized, and accessible.
And I expect new tools will be published, in the near future.
Glauco
Samiro Discher
Mar 11, 2023, 2:07:09 PM3/11/23
to Metamath
> In the longer term I'd like to create a nonprofit association to manage
these things. The goal would be to set up something that could outlive
us all. Its notional purpose would be something like "Enable and
encourage computer-verified formalization of mathematics.".
This is an excellent idea, I'd be totally in support of that. I find it puzzling that so many mathematicians do not seem to care to formalize their work in order to make it objectively verifiable, convertible, applicable, etc. via computing.
Also, thank you for your great work, David, and to all the other contributors that are — in my perception — working on fundamentally improving our formal sciences.
--- Samiro Discher
Reply all
Reply to author
Forward
0 new messages