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

11–20 of 44 posts

Re: Palomar: A registry of Lean verified mathematics

#11

Post by sva_ »

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

Re: Palomar: A registry of Lean verified mathematics

#12

Post by dsfadgergdsg »

sva_ wrote: post #11

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

[flagged]

Re: Palomar: A registry of Lean verified mathematics

#13

Post by JuniperMesos »

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

Re: Palomar: A registry of Lean verified mathematics

#15

Post by fuglede_ »

JuniperMesos wrote: post #13

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

Re: Palomar: A registry of Lean verified mathematics

#16

Post by teiferer »

sva_ wrote: post #11

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

Re: Palomar: A registry of Lean verified mathematics

#18

Post by JohnKemeny »

teiferer wrote: post #16
sva_ wrote: post #11

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

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?

Re: Palomar: A registry of Lean verified mathematics

#19

Post by kachnuv_ocasek »

JuniperMesos wrote: post #13

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

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

Re: Palomar: A registry of Lean verified mathematics

#20

Post by klntsky »

fuglede_ wrote: post #15
JuniperMesos wrote: post #13

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

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