LeanDojo: Theorem Proving in Lean Using LLMs • Hacker News Board

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#51

Post by ithkuil » Tue, Jul 30, 2024, 2:21 AM UTC

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.

People are not neurons.

Intelligent systems (once eventually devised) will use computation machines as the substrate to implement intelligence in a similar way as the human intelligence uses a biological substrate to perform gazillions of individually unintelligent computations.

Don't confuse the substrate for the system

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#52

Post by [deleted] » Tue, Jul 30, 2024, 10:37 AM UTC

thomasahle wrote: post #49

Davidzheng wrote: post #32

Earlier quoted context omitted.

I'm not sure if you're confusing alphaproof with leandojo here? Alphaproof generated its own proofs on 100M formal problems and did RL on this process.

Yes, I know AlphaProof did that. I wrote that it would be exciting "if they [LeanDojo] could integrate the reinforcement learning approach from AlphaProof". This would give LeanDojo a lot more training data, and hopefully give us an open source proof assistant at IMO Silver level.

[deleted]

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#53

Post by pfdietz » Tue, Jul 30, 2024, 12:21 PM UTC

staunton wrote: post #42

ijustlovemath wrote: post #39

Earlier quoted context omitted.

The big problem with this is that many domains of math use hyper specialized notation, novel terms, different styles etc, and there's not much data for them to train on within any given niche. For example, the IUT "proof" of the abc conjecture used completely novel systems to come to its conclusions, to the point that it took top number theorists a few years to even parse what it was saying, and only then could they…

> if you can find the problem in the proof Is it still open whether there is a problem? Last I heard about this, there was one guy saying there's problems and the author dismissing that as "they just didn't understand it" without showing much interest in explaining it better...

Given his behavior, I wouldn't believe anything from that guy unless it came with a formalized proof.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#54

Post by Davidzheng » Wed, Jul 31, 2024, 5:51 PM UTC

thomasahle wrote: post #49

Davidzheng wrote: post #32

Earlier quoted context omitted.

I'm not sure if you're confusing alphaproof with leandojo here? Alphaproof generated its own proofs on 100M formal problems and did RL on this process.

Yes, I know AlphaProof did that. I wrote that it would be exciting "if they [LeanDojo] could integrate the reinforcement learning approach from AlphaProof". This would give LeanDojo a lot more training data, and hopefully give us an open source proof assistant at IMO Silver level.

Sorry!

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#55

Post by staunton » Thu, Aug 01, 2024, 8:34 AM UTC

pfdietz wrote: post #53

staunton wrote: post #42

Earlier quoted context omitted.

> if you can find the problem in the proof Is it still open whether there is a problem? Last I heard about this, there was one guy saying there's problems and the author dismissing that as "they just didn't understand it" without showing much interest in explaining it better...

Given his behavior, I wouldn't believe anything from that guy unless it came with a formalized proof.

If you mistrust authors and can't actually rule out someone trying to cheat, checking a formaized proof beyond a reasonable doubt is still a lot of work and needs a huge amount of domain-specific knowledge. An author trying to cheat would try to make everything chaotic and hard to read, as well as hiding subtle flaws in theorem statements.