Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Palomar: A registry of Lean verified mathematics

terrytao.wordpress.com

Post reply on HN
Print view View original

31–40 of 44 posts

Re: Palomar: A registry of Lean verified mathematics

#31

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

Re: Palomar: A registry of Lean verified mathematics

#33

Post by emil-lp »

demibabs wrote: post #5

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

Re: Palomar: A registry of Lean verified mathematics

#34

Post by bebimbop »

klntsky wrote: post #20
fuglede_ wrote: post #15

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

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.

Re: Palomar: A registry of Lean verified mathematics

#35

Post by steinwinde »

YetAnotherNick wrote: post #30
crote wrote: post #28

Earlier quoted context omitted.

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.

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

Re: Palomar: A registry of Lean verified mathematics

#36

Post by fuglede_ »

steinwinde wrote: post #22
klntsky wrote: post #20

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

> 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 mechanis…

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.

Re: Palomar: A registry of Lean verified mathematics

#37

Post by orochimaaru »

crote wrote: post #28
klntsky wrote: post #20

Earlier 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…

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.

Re: Palomar: A registry of Lean verified mathematics

#38

Post by orochimaaru »

zldar wrote: post #24
fuglede_ wrote: post #15

Earlier quoted context omitted.

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.

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.
Post reply on HN