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

LeanDojo: Theorem Proving in Lean Using LLMs

leandojo.org

Post reply on HN
Print view View original

11–20 of 55 posts

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#11

Post by ijustlovemath »

sva_ wrote: post #7
ijustlovemath wrote: post #5

Earlier quoted context omitted.

This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.

> if baked deep into an ML's kernel/structure/training process Not sure of the feasibility of implementing lean as a GPU kernel, if you meant that. Also I'm not sure it makes sense to run Lean inside the (mostly matmul) training process. Now to use it to prepare some training data, it seems more realistic. But that seems to be what AlphaProof tries to do in the reinforcement step, if I'm not mistaken.

I think that in order for it to truly find deep insights, it would need to do more than just generate training data. I'm also a believer that the current AI approaches are approaching their limits as the human feed dries up and we start using old models to train new ones.

Of course, what that really means and how you'd go about adapting your CUDA code / hardware, would have to be researched.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#12

Post by ijustlovemath »

mathinaly wrote: post #6
ijustlovemath wrote: post #5

Earlier quoted context omitted.

This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.

It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. It will loop forever looking for a proof that will never show up in the search. Computers are useful for doing fast calculations but attributing intelligence to them beyond that is mostly a result of confused ontologies and metaphysics about what computers are capable of do…

Perhaps true of the class of problems that are undecidable in, say, the Peano axioms / ZFC. However, there are many things these axioms can prove that are still useful! For example, the multiplicity of the totient function, applications of which power much of modern cryptography.

Riemann is so widely believed to be true that there are entire branches of mathematics dedicated to seeing what cool things you can learn about primes/combinatorics etc by taking Riemann to be true as an assumption.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#13

Post by skissane »

mathinaly wrote: post #6
ijustlovemath wrote: post #5

Earlier quoted context omitted.

This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.

It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. It will loop forever looking for a proof that will never show up in the search. Computers are useful for doing fast calculations but attributing intelligence to them beyond that is mostly a result of confused ontologies and metaphysics about what computers are capable of do…

> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own.

Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same.

If the Riemann hypothesis is independent of ZFC, and there exists a proof of that independence which is of tractable length, then in principle if a human could discover it, why couldn’t a sufficiently advanced computer system?

Of course, it may turn out either that (a) Riemann hypothesis isn’t independent of ZFC (what most mathematicians think), or (b) it is independent but no proof exists, or (c) the shortest proof is so astronomically long nobody will ever be able to know it

> The incompleteness theorem for example is a meta-mathematical statement about the limits of axiomatic systems that can not be discovered with axiomatic systems alone.

We have proofs of Gödel‘s theorems. I see no reason in principle why a (sufficiently powerful) automated theorem prover couldn’t discover those proofs for itself. And maybe even one day discover proofs of novel theorems in the same vein

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#14

Post by mathinaly »

skissane wrote: post #13
mathinaly wrote: post #6

Earlier quoted context omitted.

It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. It will loop forever looking for a proof that will never show up in the search. Computers are useful for doing fast calculations but attributing intelligence to them beyond that is mostly a result of confused ontologies and metaphysics about what computers are capable of do…

> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same. If the Riemann hypothesis is independent of ZFC, and there exists a proof…

No computer has ever discovered the concept of a Turing machine and the associated halting problem (incompleteness theorem). If you think a search in an axiomatic system can discover an incompleteness result it is because your ontology about what computers can do is confused. People are not computers.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#16

Post by thomasahle »

ijustlovemath wrote: post #5
thomasahle wrote: post #3

I wonder if they could integrate with the reinforcement learning approach from AlphaProof (this week). Having an IMO silver level proof copilot would pretty neat!

This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success. Privately, I think Lean could be incredibly powerful if baked deep into an ML's kernel/structure/training process. I think an AI proof of something like the Riemann Hypothesis may well be possible if you get enough resources behind it.

> This is precisely how Google built AlphaProof! Read the article, Lean's role is quite critical to its success.

I read the article. It doesn't say anything about generating new proofs to train on. It only mentions scraping Github for lean theorems+proofs.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#17

Post by bubblyworld »

mathinaly wrote: post #14
skissane wrote: post #13

Earlier quoted context omitted.

> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same. If the Riemann hypothesis is independent of ZFC, and there exists a proof…

No computer has ever discovered the concept of a Turing machine and the associated halting problem (incompleteness theorem). If you think a search in an axiomatic system can discover an incompleteness result it is because your ontology about what computers can do is confused. People are not computers.

To be pedantic (mathematical?), computers can find any result that has a formalisation in a finitary logical systems like first-order logic, simply by searching all possible proofs. Undecidability of FOL inference isn't relevant when you already know such a proof exists (it's a "semidecidable" problem).

I imagine that would be the main use case for heuristic solvers like this one - helping mathematicians fill in the blanks in proofs for stuff that's not too tricky but annoying to do by hand. Rather than for discovering novel, unknown concepts by itself (although I'm with the OP, don't see why this is impossible a priori).

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#18

Post by bubblyworld »

skissane wrote: post #13
mathinaly wrote: post #6

Earlier quoted context omitted.

It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. It will loop forever looking for a proof that will never show up in the search. Computers are useful for doing fast calculations but attributing intelligence to them beyond that is mostly a result of confused ontologies and metaphysics about what computers are capable of do…

> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same. If the Riemann hypothesis is independent of ZFC, and there exists a proof…

Bahaha it would be great if RH turned out to be a natural example of a theorem for which its independence is itself independent of ZFC. Do you know any examples of that?

I can probably cook some highly artificial ones up if I try, but maybe there's an interesting one out there!

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#19

Post by skissane »

bubblyworld wrote: post #18
skissane wrote: post #13

Earlier quoted context omitted.

> It's possible that the hypothesis is independent of the existing axiomatic systems for mathematics and a computer can't discover that on its own. Humans have discovered independence proofs, e.g. Paul Cohen’s 1963 proof that the continuum hypothesis is independent of ZFC. I can’t see any reason in principle why a computer couldn’t do the same. If the Riemann hypothesis is independent of ZFC, and there exists a proof…

Bahaha it would be great if RH turned out to be a natural example of a theorem for which its independence is itself independent of ZFC. Do you know any examples of that? I can probably cook some highly artificial ones up if I try, but maybe there's an interesting one out there!

> turned out to be a natural example of a theorem for which it's independence is itself independent of ZFC. Do you know any examples of that?

Not aware of any myself, no. (But I’m far from an expert on this topic.)

It just occurred to me as a logical possibility.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#20

Post by mathinaly »

bubblyworld wrote: post #17
mathinaly wrote: post #14

Earlier quoted context omitted.

No computer has ever discovered the concept of a Turing machine and the associated halting problem (incompleteness theorem). If you think a search in an axiomatic system can discover an incompleteness result it is because your ontology about what computers can do is confused. People are not computers.

To be pedantic (mathematical?), computers can find any result that has a formalisation in a finitary logical systems like first-order logic, simply by searching all possible proofs. Undecidability of FOL inference isn't relevant when you already know such a proof exists (it's a "semidecidable" problem). I imagine that would be the main use case for heuristic solvers like this one - helping mathematicians fill in the…

Because meta-mathematical proofs often use transcendental induction and associated "non-constructive" and "non-finitistic" arguments. The diagonilization argument itself is an instance of something that can not actually be implemented on a computer because constructing the relevant function in finite time is impossible. Computers are great but when people say things like "The human mind is software running on the brain like a computer" that indicates to me they are confused about what they're trying to say about minds, brains, and computers. Collapsing all those different concepts into a Turing machine is what I mean by a confused ontology.

In any event, I'm dropping out of this thread since I don't have much else to say on this and it often leads to unnecessary theorycrafting with people who haven't done the prerequisite reading on the relevant matters.

Post reply on HN