> 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.
> 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.
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?
Why publish research articles? Why contribute to the Linux kernel? ...?
Same reason why you would use arxiv instead of posting the result to X.