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

41–50 of 55 posts

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#41

Post by umutisik »

fsndz wrote: post #34

What's a real-life use case of theorem proving ? I really want to learn more about that but it always feel like an abstract thing that people do because they like solving puzzles. Does it help in solving the reliability challenge of current LLMs ( https://www.lycee.ai/blog/ai-reliability-challenge ) ?

Real life use cases for theorem proving I am aware of: - Formal verification of implementations for applications that require extreme security and reliability. (banking, aerospace, ...) - Automated theorem proving would increase the pace of theoretical work. In some cases, that helps guide useful work. There are better examples, but a simple one: nobody is looking for faster (worst-case) sorting algorithms because there is a proven theoretical limit. Don't believe in theory, but don't be without theory! It definitely won't hurt if theory-building is cheaper and faster.

Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#42

Post by staunton »

ijustlovemath wrote: post #39
pfdietz wrote: post #33

Earlier quoted context omitted.

I want to see a system that automates formalization of the existing math literature. LLMs are supposed to be good on language, right? So get them to read math papers and fill in the blanks, spitting out formalized versions of the results in Lean. We have centuries of literature to process, and when we're done there will be all of mathematics formalized to serve as training data for theorem provers moving into new mat…

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

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#43

Post by butokai »

worldsayshi wrote: post #9

Victor Taelin is doing some semi-related stuff with Claude and their home built proof language Kind2: https://x.com/VictorTaelin/status/1811167900780175423 Can recommend taking a look at their recorded Twitch stream to see it in action.

That's really cool. Having spent most of my time in (european) academia, I wonder how this kind of research can be carried out outside of academic institutions.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#44

Post by jcla1 »

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

I recon the general cosensus among mathematicians (as that is what counts) is that the ABC conjecture so far has _not_ been proven. Mochizuki (and his school around him) seem to be the majority of people that believe his proof is correct. As you point out, Scholze has identified a supposed flaw in Mochizuki's argument, but anyone not already at the forefront of IUT/NT/ABC conjecture is probably incapable of telling if this flaw is a true flaw or not. As Mochizuki refuses to elaborate (on this supposed flaw) consensus cannot be reached and thus the ABC conjecture remains open.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#45

Post by summerlight »

fsndz wrote: post #34

What's a real-life use case of theorem proving ? I really want to learn more about that but it always feel like an abstract thing that people do because they like solving puzzles. Does it help in solving the reliability challenge of current LLMs ( https://www.lycee.ai/blog/ai-reliability-challenge ) ?

When you want near 100% confidence on your design, you're gonna need formal method or something similar. Usually this is meant for critical, complex infrastructures and AWS has been one of such organization. https://www.amazon.science/publications/how-amazon-web-servi...

This can be applied on something like: Is your extension on distributed system protocol (like Paxos) correct? Does my novel security system hold certain properties? etc etc...

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#46

Post by brotchie »

How good is Lean at assisting the analytical solution to PDEs?

10+ years out from a Finance PhD where I ended up using numerical methods because I really didn't have the math skills to prove closed form solutions.

Would love to know if, starting with a stochastic differential equation, how far your can go re: applying Ito's lemma and working through the math to get to a closed form solution (using Lean).

It the main advantage of Lean (ignoring LLM assistance) that you build up declarative code that, as you incrementally work on the proof, guarantees that the proof-so-far is correct?

So you're still "working through the math" but rather than un-executable math notation written on a pad, you have "by induction" a guaranteed valid argument up to the point you are at in the proof?

Just trying to build a mental model of Lean > pen and pad.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#47

Post by mccoyb »

brotchie wrote: post #46

How good is Lean at assisting the analytical solution to PDEs? 10+ years out from a Finance PhD where I ended up using numerical methods because I really didn't have the math skills to prove closed form solutions. Would love to know if, starting with a stochastic differential equation, how far your can go re: applying Ito's lemma and working through the math to get to a closed form solution (using Lean). It the main…

Not quite a positive (it's ready now!) answer, but there's some interesting work on denoting problems, and constructing numerical methods for systems like the one you're describing -- I believe the design of this library (while not yet mature) would support the workflow you described (including both analytic and numerical solutions):

https://github.com/lecopivo/SciLean

To your last point, the idea is that numerical approximations can be introduced (and introduction will ask for proofs of validity! but you can ignore "the proving" via `sorry`) to go from un-executable math notation (in Lean4) to executable!

Whether the proof goes through doesn't affect the final executable.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#48

Post by maxwells-daemon »

gnahtb wrote: post #27
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

LeanDojo (at least as original published) did not use automatically formalized data, but extracted examples from Mathlib, which is already written in Lean.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#49

Post by thomasahle »

Davidzheng wrote: post #32
thomasahle wrote: post #16

Earlier quoted context omitted.

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

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.

Re: LeanDojo: Theorem Proving in Lean Using LLMs

#50

Post by thomasahle »

namibj wrote: post #36
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!

Are you offering to code that or donate compute for the RL training? The problem is mostly that it's fairly intensive to code an efficient RL trainer for this, and even then it's expensive to run the training.

Maybe it could be done distributed, in a similar way to the Leela Zero open source replication of Alpha Zero.
Post reply on HN