Hacker News Reader

Comment by fjfaase | Hacker News Reader

I think that something like http://us.metamath.org/index.html has already gone a long way in formalizing math. And this is not the only attempt to formalize math, but it is unique that it uses a very limited amount of syntax and rules, and makes use of a simple (small) proof engine, which makes verifying that the proof engine is correct possible.

View on HN

The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.

> The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves.

While it's allowed, generally Metamath users do not prove constructs directly from axioms, for exactly the same reason as you don't do it in Lean or traditional informal mathematics. You're right that most Metamath tools have fewer automated tactics, but there are tools with some automation, and people are working to improve that.

A small proof engine, and maybe a limited amount of rules (depending on the exact technical meaning of 'rules') is a good thing, but I'd say a limited amount of syntax is a bad thing. Mathematicians as a community tend to be happy with—I might even say to prefer—lots of syntax, and, if you want to get a formalisation process really going, layering it with enough syntactic sugar to bring in mathematicians who aren't usually 'formalisers' is going to be essential.

It's also true that there are lots of attempts at formalisation out there; I happen to know about vdash.org , for example, but there are certainly others. I think it's good to have an abundance of formalisations, since no one formalisation style is going to appeal to everyone (for example, as already discussed above, probably the more formalisation-minded mathematicians will have a higher tolerance for minimalism).

Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]).

Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath.

[1] https://github.com/gebner/trepplein/tree/master/src/main/sca...

Reply on news.ycombinator.com