> A zeroth approximation of what Palomar intends to be is the analogue of a preprint server for Lean proofs. More precisely, Palomar (which is named after the astronomical observatory) is a registry of external Github repositories (or more precisely, “snapshots” of such repositories, as represented by a specific Github commit) containing Lean code adhering to the current best practices for such formalizations,
Either Terry Tao is - imprecisely and inaccurately - using the name of the popular git repository hosting service "Github" as a synonym for the open-source version control system "git", likely because he has some familiarity with software version control but is not himself a specialist in computer programming; or he does fully understand the distinction and Palomar was written in such a way that it only works for git repositories hosted on GitHub specifically and Tao is accurately describing that. Either possibility is unfortunate. I do not like GitHub's de-facto mindshare monopoly on decentralized version control system hosting.
> The submission process is thorough, but achievable: as a test, I successfully managed to submit my own recent formalization [...]
I find this kind of endearing, how he almost makes it sounds like "If even I can do it, you can too!", disregarding he's probably the most prolific mathematician currently alive.
Some years ago I suggested it might be interesting to have a kind of blockchain of formally verifiable mathematical proofs, but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems.
I think the larger issue of computationally creating a library of math proofs is still that one might come up with an infinite amount of useless theorems that are trivial to prove, but I suppose this registry is manually vetted. Theres a strong inductive bias in maths in that humans still decide what axiomatic systems, theorems, definitions etc are interesting to us.
But I think the method of proving things will soon go out style as an endeavor to devote perhaps years of your life to.
> 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.
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.
Either Terry Tao is - imprecisely and inaccurately - using the name of the popular git repository hosting service "Github" as a synonym for the open-source version control system "git", likely because he has some familiarity with software version control but is not himself a specialist in computer programming; or he does fully understand the distinction and Palomar was written in such a way that it only works for git repositories hosted on GitHub specifically and Tao is accurately describing that. Either possibility is unfortunate. I do not like GitHub's de-facto mindshare monopoly on decentralized version control system hosting.
I find this kind of endearing, how he almost makes it sounds like "If even I can do it, you can too!", disregarding he's probably the most prolific mathematician currently alive.
Some years ago I suggested it might be interesting to have a kind of blockchain of formally verifiable mathematical proofs, but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems.
I think the larger issue of computationally creating a library of math proofs is still that one might come up with an infinite amount of useless theorems that are trivial to prove, but I suppose this registry is manually vetted. Theres a strong inductive bias in maths in that humans still decide what axiomatic systems, theorems, definitions etc are interesting to us.
But I think the method of proving things will soon go out style as an endeavor to devote perhaps years of your life to.
Isn’t this kind of a recursive problem where you now have to prove your proof that their proof proves their claimed statement?
Seems to be doing exactly the same?
https://us.metamath.org/
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.