Palomar: A Registry for Lean-Verified Mathematics Opens for Submissions
Palomar: A registry of Lean verified mathematics
Terence Tao announces the launch of Palomar, a registry for Lean-verified mathematics, incubated by Lean FRO and ICARM. It accepts external GitHub repositories containing Lean code that proves specific results, with automated checks to ensure proofs typecheck and informal descriptions match. The registry aims to bring clarity to the growing number of AI-generated proofs, though it is not a peer-reviewed journal. Tao serves on its scientific advisory board and has already submitted his formalization of Sendov's conjecture.
A zeroth approximation of what Palomar intends to be is the analogue of a preprint server for Lean proofs.
- JuniperMesos
> 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.
- sva_
> 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.
- cbondurant
I can only hope that the hard github dependency can be chalked up to just "this was the easiest way to get this out the door". Its not a good solution in the long term, (single point of failure, github is increasingly unreliable and disliked, what about people already on a different forge or repository source) but it does solve at least a few problems that would otherwise be thorny (minimum bar for submission, outsourcing identity and spam management to github, etc.)
And since the bar for validation is expressly stated to be rather weak, I guess this would be best conceptualized as a specialized search engine that can weed out the <80th percentile of mediocre formalized proofs, with a target audience of professional mathematicians who have the ability to make determinations on the final 20% themselves.
Maybe also something I'd wanna skim over at some point, as a non-mathmatician who just thinks lean is neat. Its not useful to me but its fun to learn about.
- bramhaag
It seems that Lean keeps re-inventing everything Isabelle has had for decades (https://isa-afp.org/) in worse ways. There is no reason this has to depend on GitHub.
- dwheeler
Very cool. The metamath community tends to centralize results, so its equivalent is simply: