5 ms·

> 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

> 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.

fuglede_ 2mo ago
It only works for GitHub; see https://palomar-registry.org/how-to-submit https://palomar-registry.org/how-to-submit And what a strange decision indeed.
- klntsky 2mo ago
  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.
  - steinwinde 2mo ago
    > suffer whenever either of the sources goes unreachable This is not the way Palomar works. From the About page (https://palomar-registry.org/about 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.
    - fuglede_ 2mo ago
      And since all they need is a particular folder structure, you don't really need anything Git at all. Any kind of blob would do, cf. e.g. how Zenodo works.
  - crote 2mo ago
    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.
    - YetAnotherNick 2mo ago
      > 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.
      - steinwinde 2mo ago
        > on a long enough time horizon Gitlab or other provider isn't significantly better I suspect the same. But do you have any evidence for this? The status pages of Github and Gitlab (more precisely their history pages) don't seem to be a good starting point for comparisons. Anything I find online are people reporting their own experiences, and it's difficult to tell how accurate they are, how many users were truely affected etc. The only thing I can vouch for is that Github has got more unreliable - adding to the hearsay myself...
    - orochimaaru 2mo ago
      This is for mathematicians and not software engineers. You look for ease of use and familiarity with tooling. If I was a mathematician looking for a simple solution, I would go for GitHub too. Software engineering concerns don’t really apply here.
  - bebimbop 2mo ago
    I don't know if I'd consider GitLab, Bitbucket or any of the other git repo hosting services to be much worse than github in terms of availability or reliability.
- zldar 2mo ago
  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/ https://unlocked.microsoft.com/ai-anthology/terence-tao/ He clearly loves big industry, as unfortunately also too many software engineers do.
  - orochimaaru 2mo ago
    He is a fields medal winner who is looking to see how AI can further mathematics research. I’m unsure of what your specific issue with that is.
kachnuv_ocasek 2mo ago
I don't think these two possibilities are entirely exclusive. He could be using GH as a synonym for Git, but it's also the case the Palomar only works for GH repositories
biimugan 2mo ago
It requires GitHub because it forks the submission repo to keep its own immutable copy. It's just using GitHub as a costless datastore. It was probably just done that way to keep things fast and simple and get something out there as quickly as possible. There are only 15-16 verified submissions so far, so it's not like this needs something complicated yet

fuglede_ 2mo ago

It only works for GitHub; see https://palomar-registry.org/how-to-submit https://palomar-registry.org/how-to-submit And what a strange decision indeed.

klntsky 2mo ago
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.
- steinwinde 2mo ago
  > suffer whenever either of the sources goes unreachable This is not the way Palomar works. From the About page (https://palomar-registry.org/about 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.
  - fuglede_ 2mo ago
    And since all they need is a particular folder structure, you don't really need anything Git at all. Any kind of blob would do, cf. e.g. how Zenodo works.
- crote 2mo ago
  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.
  - YetAnotherNick 2mo ago
    > 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.
    - steinwinde 2mo ago
      > on a long enough time horizon Gitlab or other provider isn't significantly better I suspect the same. But do you have any evidence for this? The status pages of Github and Gitlab (more precisely their history pages) don't seem to be a good starting point for comparisons. Anything I find online are people reporting their own experiences, and it's difficult to tell how accurate they are, how many users were truely affected etc. The only thing I can vouch for is that Github has got more unreliable - adding to the hearsay myself...
  - orochimaaru 2mo ago
    This is for mathematicians and not software engineers. You look for ease of use and familiarity with tooling. If I was a mathematician looking for a simple solution, I would go for GitHub too. Software engineering concerns don’t really apply here.
- bebimbop 2mo ago
  I don't know if I'd consider GitLab, Bitbucket or any of the other git repo hosting services to be much worse than github in terms of availability or reliability.
zldar 2mo ago
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/ https://unlocked.microsoft.com/ai-anthology/terence-tao/ He clearly loves big industry, as unfortunately also too many software engineers do.
- orochimaaru 2mo ago
  He is a fields medal winner who is looking to see how AI can further mathematics research. I’m unsure of what your specific issue with that is.

kachnuv_ocasek 2mo ago

I don't think these two possibilities are entirely exclusive. He could be using GH as a synonym for Git, but it's also the case the Palomar only works for GH repositories

biimugan 2mo ago

It requires GitHub because it forks the submission repo to keep its own immutable copy. It's just using GitHub as a costless datastore. It was probably just done that way to keep things fast and simple and get something out there as quickly as possible. There are only 15-16 verified submissions so far, so it's not like this needs something complicated yet