Where is the fashionable mathematics?

[David A. Wheeler]

Fyi, There is an interesting essay about math formulas ation here:
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/

There is a discussion about it here:
https://news.ycombinator.com/item?id=22390486
--- David A.Wheeler

[Jim Kingdon]

It is a great call to arms (both the original blog post, and your response, David).

I don't think I have a lot of suggestions other than "keep formalizing things, building up as many fields of mathematics as we can". Well, and working to improve tools and all the other things we do. There is a large amount of critical mass involved in making these tools (and their proof databases) big enough and capable enough to "do mathematics" in a fuller sense. With each proof or tool improvement we get one step closer, and I like to think that my own efforts have their small contribution to make in bridging the gap between the world of constructive mathematics (which often uses type theory) and textbook understanding (which most often is set theory with excluded middle). But it is just one piece in a very large world.

As for communication tools and whether mailing lists are too old school, I hope we've made one step forward by getting on github (at least, speaking for myself I'm not sure I would have made it over the hump of becoming a contributor without github). If I set up a Slack workspace, would anyone join it? (Slack is a chat room platform often used within companies but also sometimes in community contexts, with a decent free tier). Or perhaps there already is a slack workspace for math stuff and I just don't know about it?

[Raph Levien]

Perhaps somewhat off-topic, but Zulip seems to already be a tool of choice, is the primary chat space for both Lean and Coq. We have one set up for xi and druid (xi.zulipchat.com) I find it very good. It's open to all with a github account, and we haven't had a single case of a spammy or abusive signup, out of 932 so far.

It is free for open source projects, and I'm happy to put in a word of recommendation. (I loosely know the developers)

Btw Kevin's impassioned rant is also very interesting. I seriously wonder whether dependent type theory is the best foundation for "real mathematics" though strongly appreciate the lure of it. Some of the discussion on HN is interesting but it seemed to go off the rails thanks to one "designated asshole" - what do presidential election choices and amphetamines have to do with the topic of making formalized mathematics accessible to larger groups of mathematicians?

Raph

--
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/5489D299-C6C9-400A-B29B-18D0CCA47022%40panix.com.

[Norman Megill]

I'll recall that vvs mentioned this on Feb. 10:  https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/h9PRflr9FgAJ

https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/:  "What if an undergraduate wants to try formalising the Hilbert basis theorem?  What do they do?"  Well, possibly they might look to http://us.metamath.org/mpeuni/hbt.html for some hints.  :)  BTW one purpose of the "Quantum Logic Explorer" (ql.mm) was to verify some proofs for a couple of papers, because the logic can be somewhat non-intuitive, and I don't think I'd have peace of mind not knowing if there was a flaw in one of my published claims.  On several occasions I wrote the short, informal published proof using the formal proof as a guide.  The formal proof, in turn, was based on scribbles on paper that sometimes I'd discover were wrong.

https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/:  "It will probably cost hundreds of millions of pounds worth of person-hours to digitise any one of the known proofs of Fermat’s Last Theorem, and once digitised, these proofs will need maintaining, like any software, which will cost more money."
A curious estimate - I wonder why he thinks it would be that much.  Although if the formalization language is stable, it shouldn't need "maintaining", unlike ordinary software in which there are almost always unknown bugs remaining.  The point of a formal proof (verified with a small trusted kernel) is to eliminate the possibility of a mistake or bug; once a formal proof is completed, it is finished for all posterity, aside from any optional tweaks such as proof shortening that people may wish to make.

On https://xenaproject.wordpress.com/2019/12/07/rigorous-mathematics/ he has a link to Mario's Metamath proof of the prime number theorem.

Norm

[Mario Carneiro]

On Sat, Feb 22, 2020 at 7:22 PM Norman Megill <n...@alum.mit.edu> wrote:

I'll recall that vvs mentioned this on Feb. 10:  https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/h9PRflr9FgAJ

https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/:  "What if an undergraduate wants to try formalising the Hilbert basis theorem?  What do they do?"  Well, possibly they might look to http://us.metamath.org/mpeuni/hbt.html for some hints.  :)  BTW one purpose of the "Quantum Logic Explorer" (ql.mm) was to verify some proofs for a couple of papers, because the logic can be somewhat non-intuitive, and I don't think I'd have peace of mind not knowing if there was a flaw in one of my published claims.  On several occasions I wrote the short, informal published proof using the formal proof as a guide.  The formal proof, in turn, was based on scribbles on paper that sometimes I'd discover were wrong.

https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/:  "It will probably cost hundreds of millions of pounds worth of person-hours to digitise any one of the known proofs of Fermat’s Last Theorem, and once digitised, these proofs will need maintaining, like any software, which will cost more money."
A curious estimate - I wonder why he thinks it would be that much.  Although if the formalization language is stable, it shouldn't need "maintaining", unlike ordinary software in which there are almost always unknown bugs remaining.  The point of a formal proof (verified with a small trusted kernel) is to eliminate the possibility of a mistake or bug; once a formal proof is completed, it is finished for all posterity, aside from any optional tweaks such as proof shortening that people may wish to make.

I agree that Buzzard overestimates the cost here. At this point I've almost become accustomed to formalization to the point that nothing actually appears out of reach any more. Buzzard, Commelin, and Massot recently formalized the definition of a perfectoid space in Lean. They had geared up for a multi-year project but got it done in only six months, and the delay was mostly due to learning how to use the program and work with the system, writing things so that lean will help rather than get in the way. If I could somehow transplant Kevin Buzzard's brain into my head (or someone else who understands the proof of PNT inside out), I am reasonably confident I could do it alone within a year or two. It's much more a problem of getting the relevant knowledge of mathematics and computer proof architecture into one place, and the lean zulip chat has been tremendously helpful in that regard.

Regarding the cost of maintenance, it can mostly be rolled up with maintenance of the overall ecosystem, but it is nonzero, at least for Lean. Metamath is actually an outlier in the space of formal provers for a lot of reasons, but one of them is that there is a spec, that was written almost 30 years ago and is essentially unchanged since then. Most computer languages evolve faster than that. You can't take a proof from isabelle 2019 and run it on isabelle 2020, much less an isabelle 2000 proof. Things change in a myriad small ways, and it is important that the proofs get updated to follow along. In reality, while metamath is stable, set.mm certainly is not, and we have a similar system of centralized maintenance to keep mathboxes updated when theorems in the main part change.

Of course, it's not like the software or proofs literally rot without tending; they are still just as true as ever, but now they may run on "outdated theorems", and may be difficult to reconcile with more modern developments based on different versions of core library theorems. You end up with a state of affairs which is easily recognizable to anyone who has dealt with package version management of large and diverse software ecosystems.

 

On https://xenaproject.wordpress.com/2019/12/07/rigorous-mathematics/ he has a link to Mario's Metamath proof of the prime number theorem.

Oh nice, I hadn't noticed that. Really, there are better links to give for the formalization of PNT at this point - Jeremy Avigad / Isabelle was first, John Harrison / HOL light had the complex analysis version, then I did it in metamath, and more recently Manuel Eberl / Isabelle proved most of a number theory textbook with some significant generalizations of the PNT. But I'm flattered nonetheless. :)

Mario

[savask]

"It will probably cost hundreds of millions of pounds worth of person-hours to digitise any one of the known proofs of Fermat’s Last Theorem, and once digitised, these proofs will need maintaining, like any software, which will cost more money."
A curious estimate - I wonder why he thinks it would be that much.

We could compare it with known formalizations of large theorems, for instance, Feit-Thompson theorem. As a crude estimate, the effort took 6 years and 10 full-time workers (the number of authors in https://hal.inria.fr/hal-00816699/document :-) ). At the average pay in US being ~56000$ and one pound being ~1.3$, the total cost of the project amounts to about 2.5 million pounds. Now, the original proof of odd order theorem took 255 journal pages, and Wiles' proof of Fermat's Last Theorem is about 130 pages long, so it's hard to say if its hypothetical formalization should indeed cost "hundreds of millions". The background needed for the Feit-Thompson theorem is quite wide, but it might be the case that it's even wider for Fermat's Last Theorem, so who knows.

[Jim Kingdon]

I made a Zulip login and it seems to work well via the web or the app. So if someone wants to make a Zulip (space? channel? thingie?) for metamath discussion, I'd give that a try.

If there is no interest, I'm not hugely worried, just that I'm all for trying to talk about metamath in whatever way might be helpful.

[Thierry Arnoux]

Hi Raph, all,

I’ve also created a Zulip account.
Shall we create the Metamath organization? Who should? (= who volunteers?)
How do we move forward on this?
BR,
_
Thierry

[savask]

By the way, Metamath already has a chatroom on Gitter, set up by Mario ~4 years ago: https://gitter.im/metamath/Lobby

I'm not sure if it has been suggested before, but maybe Metamath could have an IRC channel? This protocol existed for decades, is supported by many clients (or can be accessed from a web interface), requires no Github account or registration whatsoever and is a standard choice for many opensource projects (for example, Debian and Haskell use it). There's a wide variety of tools available for maintaining IRC channels, so, for instance, it's not hard to keep all logs on the metamath server.

[Mario Carneiro]

I could create a zulip chat room, but based on experience with the gitter room it seems like the demand isn't really there. Then again, lean zulip has been much more successful than lean gitter, and the threading model works much better for multiple overlapping conversations than unstructured IRC style chat.

On Mon, Feb 24, 2020 at 12:34 AM savask <sav...@yandex.ru> wrote:

By the way, Metamath already has a chatroom on Gitter, set up by Mario ~4 years ago: https://gitter.im/metamath/Lobby

I'm not sure if it has been suggested before, but maybe Metamath could have an IRC channel? This protocol existed for decades, is supported by many clients (or can be accessed from a web interface), requires no Github account or registration whatsoever and is a standard choice for many opensource projects (for example, Debian and Haskell use it). There's a wide variety of tools available for maintaining IRC channels, so, for instance, it's not hard to keep all logs on the metamath server.

--

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/e3d69c0a-8f23-4c50-93d6-6a000434e062%40googlegroups.com.

[fl]

> [chat rooms]

Based on what is happening to WhatsApp users is it a good idea?

-- 

FL