5 ms·

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 powe

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.

mathinaly 2y ago
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.
- ijustlovemath 2y ago
  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.
- skissane 2y ago
  > 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
  - mathinaly 2y ago
    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.
    - bubblyworld 2y ago
      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).
      - mathinaly 2y ago
        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.
        skissane 2y ago
        > 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?
sva_ 2y ago
> 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.
- magicalhippo 2y ago
  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.
  - ijustlovemath 2y ago
    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
    - Vecr 2y ago
      Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
      - magicalhippo 2y ago
        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.
        namibj 2y ago
        It's fairly good at valid syntax already, and did the backtracking for a long time due to it doing tree search guided by it's predictions for how likely that tactic will end up finishing the tree leaf it's applied to.
thomasahle 2y ago
> 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.
- Davidzheng 2y ago
  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.
  - thomasahle 2y ago
    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 2y ago
      [deleted]
    - Davidzheng 2y ago
      Sorry!
dkga 2y ago
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.
pfdietz 2y ago
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 mathematics.
- ijustlovemath 2y ago
  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 find the faults in the proof. I think the IUT proof would be a great adversarial example for any of these systems; if you can find the problem in the proof, you know you've hit on something pretty powerful.
  - staunton 2y ago
    > 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...
    - jcla1 2y ago
      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.

mathinaly 2y ago

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.

ijustlovemath 2y ago
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.
skissane 2y ago
> 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
- mathinaly 2y ago
  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.
  - bubblyworld 2y ago
    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).
    - mathinaly 2y ago
      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.
      - skissane 2y ago
        > 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?

sva_ 2y ago

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

magicalhippo 2y ago
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.
- ijustlovemath 2y ago
  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
  - Vecr 2y ago
    Thankfully Lean exists, so the LLM can write that instead of the math syntax used in papers.
    - magicalhippo 2y ago
      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.
      - namibj 2y ago
        It's fairly good at valid syntax already, and did the backtracking for a long time due to it doing tree search guided by it's predictions for how likely that tactic will end up finishing the tree leaf it's applied to.

thomasahle 2y ago

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

Davidzheng 2y ago
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.
- thomasahle 2y ago
  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 2y ago
    [deleted]
  - Davidzheng 2y ago
    Sorry!

dkga 2y ago

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.

pfdietz 2y ago

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

ijustlovemath 2y ago
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 find the faults in the proof. I think the IUT proof would be a great adversarial example for any of these systems; if you can find the problem in the proof, you know you've hit on something pretty powerful.
- staunton 2y ago
  > 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...
  - jcla1 2y ago
    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.