Palomar: A registry of Lean verified mathematics

tmshapland

This is really cool! The thing I was looking for in the post is why people would contribute submissions to Palomar. What is the incentive?

seeknotfind

Wow. This is incredible. Turning the entire field of mathematics into a formalized and connected system. An index of mathematical understanding. All fields will undergo this change!!! My man Terrance Tao, I hope to contribute to your symphony of progress. If the interrelationships of this are also exposed and searchable, if it can build many bridges inside itself, then this is truly the cipher key to all that can be known.

demibabs

> However, checking that a given Lean repository actually proves the claimed statement is somewhat non-trivial, especially for an audience which is not expert in the use of Lean Isn’t this kind of a recursive problem where you now have to prove your proof that their proof proves their claimed statement?

dwheeler

Very cool. The metamath community tends to centralize results, so its equivalent is simply: https://us.metamath.org/

dash2

Is there a reason to link out to Github, rather than just storing the files oneself? I don't suppose Lean proofs are very large files.