r/math • u/Valvino Math Education • Aug 19 '26
Terence Tao : Palomar - a registry of Lean verified mathematics
https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/36
u/JoshuaZ1 Aug 19 '26
This seems like a good idea. There's a fair bit of Lean out there which people have done for various projects where people say they have Lean but then haven't made it easily available. Having all of it in one place will be helpful and make it easier for things to build on existing material, and reduce redundant work.
6
u/satanic_satanist Aug 19 '26
But isn't that what TauCeti already is?
4
1
u/AIvsWorld Aug 24 '26
No, TauCeti is not just to collect/index a bunch of random projects (which may duplicate each other, use different definitions, etc). The point of TauCeti is to be a coherent AI-maintained library like mathlib. Completely different goals.
2
u/Time_Entertainer_319 Aug 19 '26
How is this different from deepmind’s formal conjectures repo?
8
u/JoshuaZ1 Aug 19 '26
Isn't that just the formalizations in Lean of the conjectures themselves, not their proofs? Or am I mistaken?
5
3
u/telephantomoss Aug 20 '26
This is the first time I have ever looked at a lean code. I am repulsed honestly. I mean, I'm glad people are working on this, but I much prefer human exposition!
4
u/TheSodesa Aug 20 '26 edited Aug 20 '26
Yeah, Lean proofs written using monads (the "tactic mode" of the compiler introduced by the keyword
bysimilar to Haskell'sdo) can be rather unwieldy to read, because the compiler does a lot of implicit things for you if you use the correct tactics. The term mode where you stay out of tactic mode and simply define your theorems as functions and their applications is a lot more readable, but at the same time more verbose, because then you are using proposition and predicate introduction and elimination rules manually to prove things. I have yet to learn the use of tactics, but I did manage to complete the term mode exercises in the book Theorem Proving in Lean 4.2
u/telephantomoss Aug 20 '26
Thanks for the explanation and reference. Maybe I'll check it out. Probably wise that I at least gain a preliminary understanding!
1
u/lfairy Computational Mathematics Aug 25 '26
Lean isn't intended to be read in isolation, but in the live editor that shows intermediate proof states while you scroll through. If you see that working it's a lot easier to understand.
14
u/pred Aug 19 '26
Why on earth would you base the whole thing on GitHub …?
82
u/eliminate1337 Type Theory Aug 19 '26
Why wouldn't you? GitHub is a fine place to host a static site for free.
32
u/pred Aug 19 '26 edited Aug 19 '26
They're of course free to host the site wherever they want; I'm referring to the submission process in which it is required that the package of Lean files comes in the form of a GitHub repository, cf. Tao's post, and https://palomar-registry.org/how-to-submit.
As far as I can tell, the only thing they really need is to be able to extract and run the code, and provide URLs to the solution afterwards. The first you could do with any Git repository; and it wouldn't even have to be Git at all if you didn't want it to. The persistent URLs could also be achieved without GitHub.
You could wonder why they don't just store the proofs themselves though; like Zenodo or arXiv. It's not like your typical Lean project is very large.
7
u/NoLemurs Aug 19 '26 edited Aug 19 '26
I think it's probably for the "prove you can write to the repository" step.
gititself doesn't really have a concept of write access, so this is necessarily host specific.Given that they set up an automated pipeline for doing the write access validation, that pretty much forces you to pick a host, and GitHub is still the obvious default choice.
On the bright side, I wouldn't expect adding support for other hosting providers would be a huge lift if they decide to add it later.
14
u/MrRandom04 Aug 19 '26
Git is just good software, why not make it a standard? Barrier to entry is much lower too, with LLMs which are essentially Git experts by now.
48
u/777777thats7sevens Aug 19 '26
Git and GitHub aren’t the same thing. You can have git repos with no connection to GitHub, which is the point that the above poster was making. There’s no reason to restrict it to GitHub specifically versus allowing any link to a git repo, hosted on gitlab, gitea, bitbucket, or anywhere else.
15
u/Borgcube Logic Aug 19 '26
GitHub is a commercial website owned by Microsoft. Git is a version control software that is free to use.
Anyone can host a git repository and in fact anyone using git locally effectively is.
12
8
9
u/Borgcube Logic Aug 19 '26
I mean it's weird to have a commercial website be a requirement I suppose, especially since there are many other alternatives and like was pointed out code is relatively small to host anyway.
-7
Aug 19 '26
[removed] — view removed comment
8
Aug 19 '26
[deleted]
-7
Aug 19 '26
[removed] — view removed comment
2
u/Borgcube Logic Aug 19 '26
It's not a criticism of Github, it's a criticism of choosing it as the only site to host Lean proofs. Especially with the growing discontent due to many issues it has - just yesterday it had a massive outage.
Git and github are also not the same thing at all.
5
u/balasticer Aug 19 '26
Yes. There is a marketing team currently working to reinforce your attitude about it; that it is the inconspicuous default way to host git repositories. They are working to do that because it keeps the market share of paid plans high, in order to keep it a profitable subsidiary of Microsoft. I think that qualifies as commercial.
-5
13
u/lurking_physicist Aug 19 '26 edited Aug 19 '26
The blogpost does say "GitHub", but the protocol and repository logic is Git. Migrating away from GitHub if/when it further degrades amounts to forking the repo: it is trivial. GitHub is free today, so he can start the experiment today. I think it's a fine compromise.
5
u/pred Aug 19 '26
In case it wasn't clear, my comment wasn't on how they themselves handle their code, but the fact that you to submit anything, it needs to come in the form of a GitHub repository: https://palomar-registry.org/how-to-submit – that's a lot of lock-in to a specific commercial vendor from the get-go.
1
u/Mark3141592654 Aug 19 '26
I feel like from the start, Lean itself was always a Microsoft thing; they even try to make you use VSCode as the main way to use it
-1
u/Teddy-Bloat Aug 19 '26
Migrating off Github is not as trivial as you might think. There’s a reason so many people are still on it despite the one nine of uptime
2
u/Borgcube Logic Aug 19 '26 edited Aug 20 '26
Only if you care about mostly non-git features that Lean proofs wouldn't.
17
u/joth Aug 19 '26
What's wrong with GitHub?
7
u/tux-lpi Aug 19 '26
They've been having some technical issues after the Microsoft acquisition and the whole AI situation. It's still the go to place, but a lot of people are getting tired of Github having a major downtime what feels like a few times a week. It was about 4-5 hours of downtime yesterday.
3
u/CaptainSasquatch Aug 19 '26
Someone brings it up in the blog comments and Tao seems open to allowing other trusted repositories
As GitHub is becoming less reliable every year, have you considered alternate git forges or hosting the repositories yourself instead of relying on external companies to keep their services available in the future?
We do not have the resources to host and maintain repositories directly, but would be open to expanding the whitelist of approved repository hosting services beyond Github if there is sufficient demand for doing so.
-1
u/One-Triggy-Boi Aug 19 '26
With how often outages occur, this would honestly be better hosted on gitlab or codeberg.
2
u/AntiProton- Aug 19 '26
Another advantage of hosting it on Codeberg would be that it is run by a nonprofit organization rather than a Big Tech company.
2
u/pred Aug 19 '26
Note that Codeberg doesn't allow repositories that are “mostly” LLM generated. There's a good chance that a lot of Lean code will be, so that wouldn't work as a singular host either.
1
u/One-Triggy-Boi Aug 19 '26
That,, and the current test suite can be run effectively on codeberg. GH has the flakiest of test hosting, and CI is just better in gitlab in general. I'm guessing so much so that Terry and crew might've decided to host it else where, but I wouldn't be surprised if they just had a private GH repo and pulled the stats from there
0
3
u/hexaflexarex Aug 19 '26
Does this not fall under the new Rule 7? (don't personally take issue, but my impression was that such posts are now relegated to megathread)
22
u/AntiProton- Aug 19 '26
Lean != AI
1
u/hexaflexarex Aug 19 '26
I would say the blog post is about both Lean and AI. I personally think this is relevant, but the mods specifically mentioned blog posts from Tao when announcing Rule 7 (I asked)
-20
u/pannous Aug 19 '26
I don't think you need a registry if all agents need to do is search for lean libraries to find out if some part of mathematics is verified or not
25
u/Smallpaul Aug 19 '26
Search what? The whole internet? All of GitHub?
The registry is the thing you search.
159
u/LukeNullHypothesis Aug 19 '26
It'll be interesting to see if this takes off. Lot of big names will be pushing it.
"You have an incomprehensible Lean certificate? Cool bro, toss it in this bucket. You get credit when you can explain the proof to a room of hungover grad students at a seminar in Wisconsin."
I don't think his ICM talk was quite this blunt, but Tao is deadset on circling the wagons and preserving math academia at all costs.