LeanDojo: Theorem Proving in Lean Using LLMs
leandojo.org
LeanDojo: Theorem Proving in Lean Using LLMs
1–10 of 55 posts
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#2Useful context: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) - "Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. "
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#3I wonder if they could integrate with the reinforcement learning approach from AlphaProof (this week). Having an IMO silver level proof copilot would pretty neat!
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#4I wonder if they could integrate with the reinforcement learning approach from AlphaProof (this week). Having an IMO silver level proof copilot would pretty neat!
I wish someone could do a cost analysis of how much compute could replicate alphaproof. Alphazero was replicated in open source, hopefully this will be too!
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#5I 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.
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#6I 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.
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 doing. Computation is a subset of mathematics and can never actually be a replacement for 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.
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#7I 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.
> 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.
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#8Earlier 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.
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.
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#9Victor 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.
Re: LeanDojo: Theorem Proving in Lean Using LLMs
#10Earlier quoted context omitted.
> 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.
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