https://xkcd.com/927/ Standards
Palomar: A registry of Lean verified mathematics
21–30 of 44 posts
Re: Palomar: A registry of Lean verified mathematics
#22Earlier quoted context omitted.
It only works for GitHub; see https://palomar-registry.org/how-to-submit And what a strange decision indeed.
No thats not a strange decision. self-hosted git servers disappear all the time, it's better to have everything unavailable at once when github is down than suffer whenever either of the sources goes unreachable. Non-developers view git availability as a simple utility, they don't attach a value judgement to git being usable with any remote.
> suffer whenever either of the sources goes unreachable
This is not the way Palomar works. From the About page (https://palomar-registry.org/about):
> Palomar does keep a public preservation fork of every registered source, solely as a backup for the registry in the event that the original repository disappears.
The decision to limit git sources to Github is likely in order to be able to use Github's fork mechanism. Palomar could still offer to take a copy of the relevant commit of non-Github repositories.
Re: Palomar: A registry of Lean verified mathematics
#23It 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.
Agreed.
Tangentially: Although many of the creators, maintainers and board members of Palomar have a background in Lean, the project welcomes alternative proof assistants, see "What about other proof assistants?" on the about (https://palomar-registry.org/about) page. From what I can tell, many in the mathematical community lament the predominance of Lean, but it reached some sort of critical mass (ecosystem, size of library) that makes it very hard to compete with - e.g. find someone who volunteers to support an alternative on Palomar, with all that this entails.
Re: Palomar: A registry of Lean verified mathematics
#24> 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…
It only works for GitHub; see https://palomar-registry.org/how-to-submit And what a strange decision indeed.
He is seemingly unbothered by the AI cartel centralization. He also wrote for MSFT's AI Anthology in 2023:
https://unlocked.microsoft.com/ai-anthology/terence-tao/
He clearly loves big industry, as unfortunately also too many software engineers do.
Re: Palomar: A registry of Lean verified mathematics
#25> 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 mathem…
> Some years ago I suggested it might be interesting to have a kind of blockchain of formally verifiable mathematical proofs, How does a blockchain help here? > but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems. I'm curious about those arguments ... what does incompleteness have to do with this? > But I think the method of proving things will soon go out st…
The Goedel bit reminded me of the bogus argument that AI is impossible due to the Goedel Incompleteness Theorem.
Re: Palomar: A registry of Lean verified mathematics
#26Wow. 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…
Every math paper ever (there are about 4 million of them) will get formalized. One benefit of this is finding out which ones were actually correct, and which had unrecognized flaws in their claimed results.
After that, we can do statistics to see which ideas in math are most used, and perhaps mine for unrecognized patterns, refactoring math to find new abstractions.
Re: Palomar: A registry of Lean verified mathematics
#27Re: Palomar: A registry of Lean verified mathematics
#28Earlier quoted context omitted.
It only works for GitHub; see https://palomar-registry.org/how-to-submit And what a strange decision indeed.
No thats not a strange decision. self-hosted git servers disappear all the time, it's better to have everything unavailable at once when github is down than suffer whenever either of the sources goes unreachable. Non-developers view git availability as a simple utility, they don't attach a value judgement to git being usable with any remote.
The main reason Github is in the news these days is due to its unreliability. If availability is your main concern, Github would be a very odd choice for your One Blessed Source.
Besides, it isn't "self-hosted basement Git server VS Github". There are plenty of other large and reliable forges out there, such as GitLab, Sourcehut, Bitbucket, or Codeberg. Considering how many people - from individual devs to major open-source projects - are abandoning Github, launching a new project in 2026 which only works with Github is a rather odd choice.
It doesn't even make sense from a technical perspective. Git has a standard protocol it uses for cloning repos. You have to go out of your way to make it not work with other forges. And if reliability is critical, surely you'd just mirror it locally? Heck, why not make use of Git's inherent distributed nature and allow defining multiple upstream sources? Integrity is already handled by the commit hash itself, so it doesn't matter if you fetch that commit from Github, GitLab, or some guy's basement server - just take whichever one happens to respond the fastest.
Re: Palomar: A registry of Lean verified mathematics
#29[dead]
Re: Palomar: A registry of Lean verified mathematics
#30Earlier quoted context omitted.
No thats not a strange decision. self-hosted git servers disappear all the time, it's better to have everything unavailable at once when github is down than suffer whenever either of the sources goes unreachable. Non-developers view git availability as a simple utility, they don't attach a value judgement to git being usable with any remote.
The main reason Github is in the news these days is due to its unreliability. If availability is your main concern, Github would be a very odd choice for your One Blessed Source. Besides, it isn't "self-hosted basement Git server VS Github". There are plenty of other large and reliable forges out there, such as GitLab, Sourcehut, Bitbucket, or Codeberg. Considering how many people - from individual devs to major open…
> Considering how many people
That is a terrible metric to look into. Github being down is news, but on a long enough time horizon Gitlab or other provider isn't significantly better. It's just they are in news less often.