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

21–30 of 55 posts

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#21

Post by skissane »

mathinaly wrote: post #20
bubblyworld wrote: post #17

Earlier quoted context omitted.

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

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

Humans reason about transcendental induction using finite time and finite resources-the human brain (as far as we know) is a finite entity. So if we can reason about the transfinite using the finite, why can’t computers? Of course they can’t do so by directly reasoning in an infinite way, but humans don’t do that, so why think computers must?

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#22

Post by dkga »

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.

Perhaps a simpler and more reachable approach at this point would be to use the mathlib documentation to fuel a RAG on top of the fine-tuned/specialised model.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#23

Post by Vecr »

ijustlovemath wrote: post #10
magicalhippo wrote: post #8

Earlier quoted context omitted.

It could perhaps also be used to guide the sampling step at the end, or? Similar to those syntax-constrained samplers to ensure the LLM spits out eg valid JSON.

Syntax constraints are usually expressible as grammars, but the language of math is often very unique and domain specific, which makes this kind of approach tricky to get right

Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#24

Post by magicalhippo »

Vecr wrote: post #23
ijustlovemath wrote: post #10

Earlier quoted context omitted.

Syntax constraints are usually expressible as grammars, but the language of math is often very unique and domain specific, which makes this kind of approach tricky to get right

Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.

So yea that was my thought. Use it to spit out valid Lean syntax, and potentially also to backtrack if it outputs inconsistent or erroneous proofs.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#25

Post by bubblyworld »

mathinaly wrote: post #20
bubblyworld wrote: post #17

Earlier quoted context omitted.

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

You don't need to implement a diagonalisation in order to prove results about it - this is true for computers as much as it is true for humans. There are formalisations of Godel's theorems in Lean, for instance. Similarly for arguments involving excluded middle and other non-constructive axioms.

I hear your point that humans reason with heuristics that are "outside" of the underlying formal system, but I don't know of a single case where the resulting theorem could not be formalised in some way (after all, this is why ZFC+ was such a big deal foundationally). Similarly, an AI will have its own set of learned heuristics that lead it to more rigorous results.

Also agree about minds and computers and such, but personally I don't think it has much bearing on what computers are capable of mathematically.

Anyway, cheers. Doesn't sound like we disagree about much.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#26

Post by altkjg »

Glad to see that major pieces of work like Lean or Wolfram Alpha are getting attention because LLMs utilize them.

Still not convinced that LLMs do anything else than rearranging other people's work.

Effects can already be seen: The Washington Post used to display articles when found via Google, now you get a paywall. And I can no longer criticize them for it.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#27

Post by gnahtb »

maxwells-daemon wrote: post #15

Second author here. Happy to answer any questions about the work!

the infographic in the deepmind blog showed the team built a formalizer network. i wonder how you guys build it. last time i tried chatgpt to translate a math problem into lean it sucks

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#28

Post by paraschopra »

bubblyworld wrote: post #25
mathinaly wrote: post #20

Earlier quoted context omitted.

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

You don't need to implement a diagonalisation in order to prove results about it - this is true for computers as much as it is true for humans. There are formalisations of Godel's theorems in Lean, for instance. Similarly for arguments involving excluded middle and other non-constructive axioms. I hear your point that humans reason with heuristics that are "outside" of the underlying formal system, but I don't know o…

what is the basic intuition of how godel's theorem are proven in Lean?

I understand OP's point of diagonalization proof being impossible to prove on a computer. (Did I get this right?)

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#29

Post by bjornsing »

altkjg wrote: post #26

Glad to see that major pieces of work like Lean or Wolfram Alpha are getting attention because LLMs utilize them. Still not convinced that LLMs do anything else than rearranging other people's work. Effects can already be seen: The Washington Post used to display articles when found via Google, now you get a paywall. And I can no longer criticize them for it.

> Still not convinced that LLMs do anything else than rearranging other people's work.

I’m not convinced that most people do anything else than rearrange other people’s work.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#30

Post by solumunus »

altkjg wrote: post #26

Glad to see that major pieces of work like Lean or Wolfram Alpha are getting attention because LLMs utilize them. Still not convinced that LLMs do anything else than rearranging other people's work. Effects can already be seen: The Washington Post used to display articles when found via Google, now you get a paywall. And I can no longer criticize them for it.

> Still not convinced that LLMs do anything else than rearranging other people's work.

It's amazing how useful and powerful that is in certain contexts.

Post reply on HN