7 ms·

Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman spe

Reconfiguring existing proofs in ways that have been tedious or obscured from humans, or using well framed methods in novel ways, will be done at superhuman speeds, and it'll unlock all sorts of capabilities well before we have to be concerned about AGI. It's going to be awesome to see what mathematicians start to do with AI tools as the tools become capable of truly keeping up with what the mathematicians want from the tools. It won't necessarily be a huge direct benefit for non-mathematicians at first, because the abstract and complex results won't have direct applications, but we might start to see millenium problems get taken down as legitimate frontier model benchmarks. Or someone like Terence Tao might figure out how to wield AI better than anyone else, even the labs, and use the tools to take a bunch down at once. I'm excited to see what's coming this year.

malux85 10mo ago
This is what has excited me for many years - the idea I call "scientific refactoring" What happens if we reason upwards but change some universal constants? What happens if we use Tao instead of Pi everywhere, these kind of fun questions would otherwise require an enormous intellectual effort whereas with the mechanisation and automation of thought, we might be able to run them and see!
- stouset 10mo ago
  > What happens if we use Tao instead of Pi everywhere Literally nothing other than mild convenience. It’s just 2pi.
  - lapetitejort 10mo ago
    Call me a mathematical extremist but I think pi should equal 6.28... and tau, which looks like half of pi, should equal 3.14...
    - measurablefunc 10mo ago
      In 1897, the Indiana General Assembly attempted to legislate a new value for pi, proposing it be defined as 3.2, which was based on a flawed mathematical proof. This bill, known as the Indiana pi bill, never became law due to its incorrect assertions and the prior proof that squaring the circle is impossible: https://en.wikipedia.org/wiki/Indiana_pi_bill https://en.wikipedia.org/wiki/Indiana_pi_bill
  - measurablefunc 10mo ago
    You're forgetting that some equations have π/2 so on balance nothing will change. It will be the same number of symbols.
    - ogogmad 10mo ago
      I don't think it's just the sheer number of symbols. It's also the fact that the symbol τ means "turn". So you can say "quarter-turn" instead of π/2. I'm not sure why that point gets lost in these discussions. And personally, I think of the set of fundamental mathematical objects as having a unique and objective definition. So, I get weirdly bothered by the offset in the Gamma function.
  - deleted 10mo ago
    [deleted]
- chmod775 10mo ago
  I can write a sed command/program that replaces every occurence of PI with TAU/2 in LaTeX formulas and it'll take me about 30 minutes. The "intellectual effort" this requires is about 0. Maybe you meant Euler's number? Since it also relates to PI, it can be used and might actually change the framework in an "interesting way" (making it more awkward in most cases - people picked PI for a reason).
  - saulpw 10mo ago
    Yeah but you also have to replace all (2*tau/2) with tau, and 4*(tau/2)^2 with tau^2, etc etc...
  - observationist 10mo ago
    I think they mean in a more general way - thinking with tau instead of pi might shift the context in terms of another method or problem solving algorithm, or there might be obscure or complex uses of tau or pi that haven't cross-fertilized in the literature - where it might be natural to think of clever extensions or use cases in one context but not the other, and those extensions and extrapolations will be apparent to AI, within reach of a tedious and exhaustive review of existing literature. I think what they were getting at is something like this: The application of existing ideas that simply haven't been applied in certain ways because it's too boring or obvious or abstract for humans to have bothered with, but AI can plow through a year's worth of human drudgery in a day or a month or so, and that sort of "brute force" won't require any amazing new technical capabilities from AI.
- sublinear 10mo ago
  * Tau
- HardCodedBias 10mo ago
  Think of how this opened up EM: https://ddcolrs.wordpress.com/2018/01/17/maxwells-equations-from-20-to-4/ https://ddcolrs.wordpress.com/2018/01/17/maxwells-equations-...
- kridsdale3 10mo ago
  Not just for math, but ALL of Science suffers heavily from a problem of less than 1% of the published works being capable of being read by leading researchers. Google Scholar was a huge step forward for doing meta-analysis vs a physical library. But agents scanning the vastness of PDFs to find correlations and insights that are far beyond human context-capacity will I hope find a lot of knowledge that we have technically already collected, but remain ignorant of.
  - newyankee 10mo ago
    Exactly, and I think not every instance can be claimed to be a hallucination, there will be so much latent knowledge they might have explored. It is likely we might see some AlphaGo type new styles in existing research workflows that AI might work out if there is some verification logic. Humans could probably never go into that space, or may be none of the researchers ever ventured there due to different reasons as progress in general is mostly always incremental.
  - zozbot234 10mo ago
    Google Scholar is still ignoring a huge amount of scholarship that is decades old (pre-digital) or even centuries old (and written in now-unused languages that ChatGPT could easily make sense of).
  - semi-extrinsic 10mo ago
    This idea is just ridiculous to anyone who's worked in academia. The theory is nice, but academic publishing is currently in the late stages of a huge death spiral. In any given scientific niche, there is a huge amount of tribal knowledge that never gets written down anywhere, just passed on from one grad student to the rest of the group, and from there spreads by percolation in the tiny niche. And papers are never honest about the performance of the results and what does not work, there is always cherry picking of benchmarks/comparisons etc. There is absolutely no way you can get these kinds of insights beyond human context capacity that you speak of. The information necessary does not exist in any dataset available to the LLM.
    - 10mo ago
- ogogmad 10mo ago
  I'm using LLMs to rewrite every formula featuring the Gamma function to instead use the factorial. Just let "z!" mean "Gamma(z+1)", substitute everywhere, and simplify. Then have the AI rewrite any prose.
  - kelipso 10mo ago
    I’m going to replace every instance of 1 with 0.999 repeating, do the equivalent for all all integers, and see how my mind totally explodes.
    - ogogmad 10mo ago
      ?
      - kelipso 10mo ago
        I thought we were all doing jokes, no?
sublinear 10mo ago
I agree only with the part about reconfiguring existing proofs. That's the value here. It is still likely very tedious to confirm what the LLMs say, but at least it's better than waiting for humans to do this half of the work. For all topics that can be expressed with language, the value of LLMs is shuffling things around to tease out a different perspective from the humans reading the output. This is the only realistic way to understand AI enough to make it practical and see it gain traction. As much as I respect Tao, I feel like his comments about AI usage can be misleading without carefully reading what he is saying in the linked posts.
- deleted 10mo ago
  [deleted]
- roadside_picnic 10mo ago
  > It is still likely very tedious to confirm what the LLMs say, A large amount of Tao's work is around using AI to assist in creating Lean proofs. I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways. One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case. We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean. This particular pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve. Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations). Personally I think strongly typed language, with powerful type systems are also the long term ideal coding with LLMs (but I'm less optimistic about devs following this path).
  - zozbot234 10mo ago
    > I don't believe that's what's happening in this specific example (and am probably wrong), but this is where a lot of Tao's enthusiasm lies. It absolutely is. With the twist that ChatGPT 5.2 can now also "explain" an AI-generated Lean proof in human-readable terms. This is a game changer, because "refactoring" can now become end-to-end: if the human explanation of a Lean proof is hard to grok and could be improved, you can test changes directly on the formal text and check that the proof still goes through for the original statement.
ComplexSystems 10mo ago
If this isn't AGI, what is? It seems unavoidable that an AI which can prove complex mathematical theorems would lead to something like AGI very quickly.
- mkl 10mo ago
  This is very narrow AI, in a subdomain where results can be automatically verified (even within mathematics that isn't currently the case for most areas).
  - threethirtytwo 10mo ago
    Narrow AI? I’m not saying it’s AGI but this is not a narrow AI it’s a general AI given a narrow problem. ChatGPT.
    - gf000 10mo ago
      In a very specialized setup, in tandem with a verifier. Just because a specialized human placed in an F-16 can fly at Mach 2.0, doesn't mean humans in general can fly.
      - threethirtytwo 10mo ago
        An apt analogy. A human is a general intelligence that can fly with an F-16. What happens when we put an artificial general intelligence in an F-16? That's what happened here with this proof.
        mkl 10mo ago
        Not really. A completely unintelligent autopilot can fly an F-16. You cannot assume general intelligence from scaffolded tool-using success in a single narrow area.
        threethirtytwo 10mo ago
xorcist 10mo ago
> Reconfiguring existing proofs in ways that have been tedious or obscured from humans, To a layman, that doesn't sound like very AI-like? Surely there must be a dozen algorithms to effectively search this space already, given that mathematics is pretty logical?
- tombert 10mo ago
  I actually know about this a bit since it was part of what I was studying with my incomplete PhD. Isabelle has had the "Sledgehammer" tool for quite awhile [1]. It uses solvers like z3 to search and apply a catalog of proof strategies and then try and construct a proof for your main proof or any remaining subtasks that you have to complete. It's not perfect but it's remarkably useful (even if it does sometimes give you proofs that import like ten different libraries and are hard to read). I think Coq has Coqhammer but I haven't played with that one yet. [1] https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
  - matu3ba 10mo ago
    1 Does this mean that Sledgehammer and Coqhammer offer concolic testing based on an input framework (say some computing/math system formalization) for some sort of system execution/evaluation or does this only work for hand-rolled systems/mathematical expressions? Sorry for my probably senseless questions, as I'm trying to map the computing model of math solvers to common PL semantics. Probably there is better overview literature. I'd like to get an overview of proof system runtime semantics for later usage. 2 Is there an equivalent of fuzz testing (of computing systems) in math, say to construct the general proof framework? 3 Or how are proof frameworks (based on ideas how the proof could work) constructed? 4 Do I understand it correct, that math in proof systems works with term rewrite systems + used theory/logic as computing model of valid representation and operations? How is then the step semantic formally defined?
    - wizzwizz4 10mo ago
      These questions are hard to understand. 1. Yes, the Sledgehammer suite contains three testing systems that I believe are concolic (quickcheck, nitpick, nunchaku), but they only work due to hand-coded support for the mathematical constructs in question. They'd be really inefficient for a formalised software environment, because they'd be operating at a much lower-level than the abstractions of the software environment, unless dedicated support for that software environment were provided. 2. Quickcheck is a fuzz-testing framework, but it doesn't help to construct anything (except as far as it constructs examples / counterexamples). Are you thinking of something that automatically finds and defines intermediary lemmas for arbitrary areas of mathematics? Because I'm not aware of any particular work in that direction: if computers could do that, there'd be little need for mathematicians. 3. By thinking really hard, then writing down the mathematics. Same way you write computer programs, really, except there's a lot more architectural work. (Most of the time, the computer can brute-force a proof for you, so you need only choose appropriate intermediary lemmas.) 4. I can't parse the question, but I suspect you're thinking of the meta-logic / object-logic distinction. The actual steps in the term rewriting are not represented in the object logic: the meta-logic simply asserts that it's valid to perform these steps. (Not even that: it just does them, accountable to none other than itself.) Isabelle's meta-logic is software, written in a programming language called ML.
Davidzheng 10mo ago
I don't think there's a real boundary between reconfiguring existing proofs and combining existing methods and "truly novel" math

malux85 10mo ago

This is what has excited me for many years - the idea I call "scientific refactoring" What happens if we reason upwards but change some universal constants? What happens if we use Tao instead of Pi everywhere, these kind of fun questions would otherwise require an enormous intellectual effort whereas with the mechanisation and automation of thought, we might be able to run them and see!

stouset 10mo ago
> What happens if we use Tao instead of Pi everywhere Literally nothing other than mild convenience. It’s just 2pi.
- lapetitejort 10mo ago
  Call me a mathematical extremist but I think pi should equal 6.28... and tau, which looks like half of pi, should equal 3.14...
  - measurablefunc 10mo ago
    In 1897, the Indiana General Assembly attempted to legislate a new value for pi, proposing it be defined as 3.2, which was based on a flawed mathematical proof. This bill, known as the Indiana pi bill, never became law due to its incorrect assertions and the prior proof that squaring the circle is impossible: https://en.wikipedia.org/wiki/Indiana_pi_bill https://en.wikipedia.org/wiki/Indiana_pi_bill
- measurablefunc 10mo ago
  You're forgetting that some equations have π/2 so on balance nothing will change. It will be the same number of symbols.
  - ogogmad 10mo ago
    I don't think it's just the sheer number of symbols. It's also the fact that the symbol τ means "turn". So you can say "quarter-turn" instead of π/2. I'm not sure why that point gets lost in these discussions. And personally, I think of the set of fundamental mathematical objects as having a unique and objective definition. So, I get weirdly bothered by the offset in the Gamma function.
- deleted 10mo ago
  [deleted]
chmod775 10mo ago
I can write a sed command/program that replaces every occurence of PI with TAU/2 in LaTeX formulas and it'll take me about 30 minutes. The "intellectual effort" this requires is about 0. Maybe you meant Euler's number? Since it also relates to PI, it can be used and might actually change the framework in an "interesting way" (making it more awkward in most cases - people picked PI for a reason).
- saulpw 10mo ago
  Yeah but you also have to replace all (2*tau/2) with tau, and 4*(tau/2)^2 with tau^2, etc etc...
- observationist 10mo ago
  I think they mean in a more general way - thinking with tau instead of pi might shift the context in terms of another method or problem solving algorithm, or there might be obscure or complex uses of tau or pi that haven't cross-fertilized in the literature - where it might be natural to think of clever extensions or use cases in one context but not the other, and those extensions and extrapolations will be apparent to AI, within reach of a tedious and exhaustive review of existing literature. I think what they were getting at is something like this: The application of existing ideas that simply haven't been applied in certain ways because it's too boring or obvious or abstract for humans to have bothered with, but AI can plow through a year's worth of human drudgery in a day or a month or so, and that sort of "brute force" won't require any amazing new technical capabilities from AI.
sublinear 10mo ago
* Tau
HardCodedBias 10mo ago
Think of how this opened up EM: https://ddcolrs.wordpress.com/2018/01/17/maxwells-equations-from-20-to-4/ https://ddcolrs.wordpress.com/2018/01/17/maxwells-equations-...
kridsdale3 10mo ago
Not just for math, but ALL of Science suffers heavily from a problem of less than 1% of the published works being capable of being read by leading researchers. Google Scholar was a huge step forward for doing meta-analysis vs a physical library. But agents scanning the vastness of PDFs to find correlations and insights that are far beyond human context-capacity will I hope find a lot of knowledge that we have technically already collected, but remain ignorant of.
- newyankee 10mo ago
  Exactly, and I think not every instance can be claimed to be a hallucination, there will be so much latent knowledge they might have explored. It is likely we might see some AlphaGo type new styles in existing research workflows that AI might work out if there is some verification logic. Humans could probably never go into that space, or may be none of the researchers ever ventured there due to different reasons as progress in general is mostly always incremental.
- zozbot234 10mo ago
  Google Scholar is still ignoring a huge amount of scholarship that is decades old (pre-digital) or even centuries old (and written in now-unused languages that ChatGPT could easily make sense of).
- semi-extrinsic 10mo ago
  This idea is just ridiculous to anyone who's worked in academia. The theory is nice, but academic publishing is currently in the late stages of a huge death spiral. In any given scientific niche, there is a huge amount of tribal knowledge that never gets written down anywhere, just passed on from one grad student to the rest of the group, and from there spreads by percolation in the tiny niche. And papers are never honest about the performance of the results and what does not work, there is always cherry picking of benchmarks/comparisons etc. There is absolutely no way you can get these kinds of insights beyond human context capacity that you speak of. The information necessary does not exist in any dataset available to the LLM.
  - 10mo ago
ogogmad 10mo ago
I'm using LLMs to rewrite every formula featuring the Gamma function to instead use the factorial. Just let "z!" mean "Gamma(z+1)", substitute everywhere, and simplify. Then have the AI rewrite any prose.
- kelipso 10mo ago
  I’m going to replace every instance of 1 with 0.999 repeating, do the equivalent for all all integers, and see how my mind totally explodes.
  - ogogmad 10mo ago
    ?
    - kelipso 10mo ago
      I thought we were all doing jokes, no?

sublinear 10mo ago

I agree only with the part about reconfiguring existing proofs. That's the value here. It is still likely very tedious to confirm what the LLMs say, but at least it's better than waiting for humans to do this half of the work. For all topics that can be expressed with language, the value of LLMs is shuffling things around to tease out a different perspective from the humans reading the output. This is the only realistic way to understand AI enough to make it practical and see it gain traction. As much as I respect Tao, I feel like his comments about AI usage can be misleading without carefully reading what he is saying in the linked posts.

deleted 10mo ago
[deleted]
roadside_picnic 10mo ago
> It is still likely very tedious to confirm what the LLMs say, A large amount of Tao's work is around using AI to assist in creating Lean proofs. I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways. One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case. We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean. This particular pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve. Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations). Personally I think strongly typed language, with powerful type systems are also the long term ideal coding with LLMs (but I'm less optimistic about devs following this path).
- zozbot234 10mo ago
  > I don't believe that's what's happening in this specific example (and am probably wrong), but this is where a lot of Tao's enthusiasm lies. It absolutely is. With the twist that ChatGPT 5.2 can now also "explain" an AI-generated Lean proof in human-readable terms. This is a game changer, because "refactoring" can now become end-to-end: if the human explanation of a Lean proof is hard to grok and could be improved, you can test changes directly on the formal text and check that the proof still goes through for the original statement.

ComplexSystems 10mo ago

If this isn't AGI, what is? It seems unavoidable that an AI which can prove complex mathematical theorems would lead to something like AGI very quickly.

mkl 10mo ago
This is very narrow AI, in a subdomain where results can be automatically verified (even within mathematics that isn't currently the case for most areas).
- threethirtytwo 10mo ago
  Narrow AI? I’m not saying it’s AGI but this is not a narrow AI it’s a general AI given a narrow problem. ChatGPT.
  - gf000 10mo ago
    In a very specialized setup, in tandem with a verifier. Just because a specialized human placed in an F-16 can fly at Mach 2.0, doesn't mean humans in general can fly.
    - threethirtytwo 10mo ago
      An apt analogy. A human is a general intelligence that can fly with an F-16. What happens when we put an artificial general intelligence in an F-16? That's what happened here with this proof.
      - mkl 10mo ago
        Not really. A completely unintelligent autopilot can fly an F-16. You cannot assume general intelligence from scaffolded tool-using success in a single narrow area.
        threethirtytwo 10mo ago

xorcist 10mo ago

> Reconfiguring existing proofs in ways that have been tedious or obscured from humans, To a layman, that doesn't sound like very AI-like? Surely there must be a dozen algorithms to effectively search this space already, given that mathematics is pretty logical?

tombert 10mo ago
I actually know about this a bit since it was part of what I was studying with my incomplete PhD. Isabelle has had the "Sledgehammer" tool for quite awhile [1]. It uses solvers like z3 to search and apply a catalog of proof strategies and then try and construct a proof for your main proof or any remaining subtasks that you have to complete. It's not perfect but it's remarkably useful (even if it does sometimes give you proofs that import like ten different libraries and are hard to read). I think Coq has Coqhammer but I haven't played with that one yet. [1] https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
- matu3ba 10mo ago
  1 Does this mean that Sledgehammer and Coqhammer offer concolic testing based on an input framework (say some computing/math system formalization) for some sort of system execution/evaluation or does this only work for hand-rolled systems/mathematical expressions? Sorry for my probably senseless questions, as I'm trying to map the computing model of math solvers to common PL semantics. Probably there is better overview literature. I'd like to get an overview of proof system runtime semantics for later usage. 2 Is there an equivalent of fuzz testing (of computing systems) in math, say to construct the general proof framework? 3 Or how are proof frameworks (based on ideas how the proof could work) constructed? 4 Do I understand it correct, that math in proof systems works with term rewrite systems + used theory/logic as computing model of valid representation and operations? How is then the step semantic formally defined?
  - wizzwizz4 10mo ago
    These questions are hard to understand. 1. Yes, the Sledgehammer suite contains three testing systems that I believe are concolic (quickcheck, nitpick, nunchaku), but they only work due to hand-coded support for the mathematical constructs in question. They'd be really inefficient for a formalised software environment, because they'd be operating at a much lower-level than the abstractions of the software environment, unless dedicated support for that software environment were provided. 2. Quickcheck is a fuzz-testing framework, but it doesn't help to construct anything (except as far as it constructs examples / counterexamples). Are you thinking of something that automatically finds and defines intermediary lemmas for arbitrary areas of mathematics? Because I'm not aware of any particular work in that direction: if computers could do that, there'd be little need for mathematicians. 3. By thinking really hard, then writing down the mathematics. Same way you write computer programs, really, except there's a lot more architectural work. (Most of the time, the computer can brute-force a proof for you, so you need only choose appropriate intermediary lemmas.) 4. I can't parse the question, but I suspect you're thinking of the meta-logic / object-logic distinction. The actual steps in the term rewriting are not represented in the object logic: the meta-logic simply asserts that it's valid to perform these steps. (Not even that: it just does them, accountable to none other than itself.) Isabelle's meta-logic is software, written in a programming language called ML.

Davidzheng 10mo ago

I don't think there's a real boundary between reconfiguring existing proofs and combining existing methods and "truly novel" math