Palomar: A registry of Lean verified mathematics
terrytao.wordpress.com
Palomar: A registry of Lean verified mathematics
1–10 of 44 posts
Re: Palomar: A registry of Lean verified mathematics
#2This is really cool! The thing I was looking for in the post is why people would contribute submissions to Palomar. What is the incentive?
Re: Palomar: A registry of Lean verified mathematics
#3This is really cool! The thing I was looking for in the post is why people would contribute submissions to Palomar. What is the incentive?
Same reason why you would use arxiv instead of posting the result to X.
Re: Palomar: A registry of Lean verified mathematics
#4Wow. 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.
Re: Palomar: A registry of Lean verified mathematics
#5> 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?
Re: Palomar: A registry of Lean verified mathematics
#6Very cool. The metamath community tends to centralize results, so its equivalent is simply:
Re: Palomar: A registry of Lean verified mathematics
#7This 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? ...?
Re: Palomar: A registry of Lean verified mathematics
#8Is 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.
Re: Palomar: A registry of Lean verified mathematics
#9> 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?
It's not a proof. You check that the mathematical ideas expressed in the claimed statement are the same as the mathematical ideas expressed by the Lean repository.
Re: Palomar: A registry of Lean verified mathematics
#10https://theoremdb.org/
Seems to be doing exactly the same?