> 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.
> 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 style as an endeavor to devote perhaps years of your life to.
I'm not in that camp. With the new tools available, it might change how this endeavor exactly works, but there will always be claims at the edge of our understanding for which we seek explanations and proofs are just that. The ones that can be easily and autonomously discovered by a machine will not be subject to human attention for that purpose, but there will still be a frontier that needs (and will get) attention.
Mind you that not all math activity happens at that frontier. Generations of aspirarional young math fans have re-proven countless foundational results just for fun, because it's a satisfying and eye-opening activity, and that's how you learn. That will not change fundamentally even though maybe the tools they use will.
It's also not new that the setting for frontier research changes. Not too many generations ago, proofs were written with literal pen on paper and communicated by letter to dear math colleagues in distant countries. That's very different today, but has not killed math as a profession. To the contrary. There are far more mathematicians today than there were 300 years ago.
Not trying to answer on OP's behalf, but perhaps they didn't mean blockchain in the literal sense, but more like a DAG of theorems that are shared globally?
Maybe some sort of blockchain could make it so that you don't have to verify the whole proof yourself, to know that it's true. Because some of these proofs could take a long time to verify. Similar to a Merkle tree, but you'd have to make it respect the laws of mathematical proof in some way.
edit: Yes I think this should be possible, using a "recursive SNARK".
> but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems
You shouldn't have listened to them, "incompleteness" only applies when you try to encode the language and meta-language in the same encoding—which no one actual does. (For example, programming language syntax is complete.)
> 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.
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.
> 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.
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.
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.
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.
> 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...
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.
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
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
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.
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.
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.
> 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.
It's nice to see Terry not only accepting the assistance of AI in mathematics but helping to strengthen the formalization infrastructure for the AI and Math communities.
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.
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.
Ah, interesting! I've been toying around with a formalizing of a paper I'm closing to submitting; maybe I'll try to clean it up into a format for this.
> 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.
> 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 style as an endeavor to devote perhaps years of your life to.
I'm not in that camp. With the new tools available, it might change how this endeavor exactly works, but there will always be claims at the edge of our understanding for which we seek explanations and proofs are just that. The ones that can be easily and autonomously discovered by a machine will not be subject to human attention for that purpose, but there will still be a frontier that needs (and will get) attention.
Mind you that not all math activity happens at that frontier. Generations of aspirarional young math fans have re-proven countless foundational results just for fun, because it's a satisfying and eye-opening activity, and that's how you learn. That will not change fundamentally even though maybe the tools they use will.
It's also not new that the setting for frontier research changes. Not too many generations ago, proofs were written with literal pen on paper and communicated by letter to dear math colleagues in distant countries. That's very different today, but has not killed math as a profession. To the contrary. There are far more mathematicians today than there were 300 years ago.
Not trying to answer on OP's behalf, but perhaps they didn't mean blockchain in the literal sense, but more like a DAG of theorems that are shared globally?
The Goedel bit reminded me of the bogus argument that AI is impossible due to the Goedel Incompleteness Theorem.
Maybe some sort of blockchain could make it so that you don't have to verify the whole proof yourself, to know that it's true. Because some of these proofs could take a long time to verify. Similar to a Merkle tree, but you'd have to make it respect the laws of mathematical proof in some way.
edit: Yes I think this should be possible, using a "recursive SNARK".
> but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems
You shouldn't have listened to them, "incompleteness" only applies when you try to encode the language and meta-language in the same encoding—which no one actual does. (For example, programming language syntax is complete.)
[flagged]
> 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.
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.
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.
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.
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.
> 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.
> 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...
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.
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.
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.
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
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
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.
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.
Very cool. The metamath community tends to centralize results, so its equivalent is simply:
https://us.metamath.org/
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.
> 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?
You only have to prove the formalization of the theorem statement. The formalized statement is guaranteed to be true if Lean says so.
There will always be a leap from the real world to the formal world.
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.
It's nice to see Terry not only accepting the assistance of AI in mathematics but helping to strengthen the formalization infrastructure for the AI and Math communities.
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.
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.
Is 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.
https://theoremdb.org/
Seems to be doing exactly the same?
Palomar requires the Comparator/formalization.yaml challenge stack. It also has an LLM-based vacuity gate backed by Tao.
Theoremdb is just a slop farm.
This 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? ...?
Articles are for academic promotion, obviously.
Same reason why you would use arxiv instead of posting the result to X.
Ah, interesting! I've been toying around with a formalizing of a paper I'm closing to submitting; maybe I'll try to clean it up into a format for this.
https://xkcd.com/927/ Standards
[dead]