Palomar: A registry of Lean verified mathematics

> 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?

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.

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.

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

https://us.metamath.org/

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?