MetaMath and Lean

Stream: new members

[Eric Taucher]

Sorry if this has been asked before, searching Zulip for this became fruitless. :frown:

Would understanding MetaMath help in learning/understanding Lean? If so, can one point to a reference or give a brief explanation of how understanding MetaMath helps for learning Lean. Thanks.

[Eric Rodriguez]

CC @Mario Carneiro - if anyone knows the answer, he does

[Huỳnh Trần Khanh]

I'm not an expert so my response shouldn't be taken as an authoritative answer on this subject. Metamath is a great site to learn how different mathematical objects are constructed in various foundations (ZFC, HOL, etc.) browsing metamath proofs is a great way to sate your curiosity, however you don't need to learn metamath to learn lean

[Huỳnh Trần Khanh]

but it wouldn't hurt of course

[Huỳnh Trần Khanh]

Mario is very familiar with Metamath, in fact he has contributed to a lot of Metamath proofs and constructions, so you should wait for him to reply :heart:

[Mario Carneiro]

@Eric Taucher The short answer: not really. The two systems are about as far apart as formal systems can get, but it can be helpful for learning how a minimalistic verifier can be used to still do "real maths". This, after all, was considered utterly infeasible in logic books as recently as the 1980s. The general concept of taking a big theorem, breaking it into tiny pieces that a computer can follow, and using lemmas to make everything scale appropriately is all applicable to any theorem prover.

Lean is a much more complicated thing than metamath and it tries to solve slightly different problems. Metamath is focused on simple verification, and there are many verifiers and a few proof assistants for it, while Lean is focused on a polished proof assistant interface, and there is only one lean tool. It invests far more heavily in a tactic infrastructure, and even the formal system itself (dependent type theory) is used to do tactic like things (definitional equality testing and type checking) in the proof kernel.

Basically, metamath is useful as a "toy example" of a theorem prover, before you try to tackle the complexity of an "industrial strength" theorem prover like lean. Or at least it feels that way when you put them side by side. Metamath is of course not just a toy, you can be just as mathematically ambitious in it as lean, but there has been way more time and effort put into the lean user experience, and it shows.

[Mario Carneiro]

By the way, I do a short comparison of Metamath and Lean in the MM0 readme, because in a lot of respects MM0 represents my attempt to merge the best aspects of both languages.