8 ms·

Machine-Assisted Proof [pdf]

199 points by jalcazar 2y ago

vessenes 2y ago
I'd call this paper a "big deal" in that it is a normalization of, very fair summary of, and indication that there is a future for, LLMs in pure mathematics from one of its leading practitioners. On HN here, we've spent the last few years talking and thinking a lot about LLMs, so the paper might not include much that would be surprising to math-curious HN'ers. However, there is a large cohort of research mathematicians out there that likely doesn't know much about modern AI; Terence is saying there's a little utility in last-gen models (GPT-4), and he expects a lot of utility out of combining next-gen models with Lean. Again, not surprising if you read his blog, but I think publishing a full paper in AMS is a pretty important moment.
- voxl 2y ago
  LLMs as they are I postulate would not work well for this. But, purpose built stochastic auto complete with a type checker to reject the junk? That could be actually useful. Funnily enough it's also a domain of application that wouldn't make any money at all. It would have to be an offline LLM that is reasonably efficient to execute locally.
  - xaml 2y ago
    Why would it not make any money?
- deleted 2y ago
  [deleted]
- Syzygies 2y ago
  Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible. I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to explain so we can generalize? Machine proofs tend to be inscrutable. While "the singularity" is unlikely anytime soon, we should recall that before the first atomic test there were calculations to insure that we didn't ignite the atmosphere. We're going to need proofs that we have control of AI, and there's an obvious conflict of interest in trusting AI's say so here. We need to understand these proofs.
  - nextos 2y ago
    This is also my take on this. IMHO, LLMs + theorem provers have the potential to make formal methods cheap enough to use more widely. And we should give more credit to the theorem prover part of the equation, which comes in part from old AI symbolic efforts.
  - vessenes 2y ago
    Interesting thoughts, thanks. It seems to me a model trained to generate Lean could also be purposed to explain a large Lean proof, and that’s very interesting. So much of modern math is limited to extremely small cohorts. None of that is dispositive inre provable safety, obviously.
  - rowanG077 2y ago
    A good thing about machine proofs is that, just like code, they can be refactored. I also use LLMs when writing code, but the code that I end up pushing is almost never exactly what the LLM has generated. I don't really see the problem with that. It's way less taxing for me mentally to get an LLM to generate definition and implementations and just refactor them quickly. I would expect LLMs for lean to be similar in the future.
jfmc 2y ago
Actually, most of the paper seems a bit obvious from the computer science side. LLMs scale for really complex tasks, but they are neither correct nor complete. If combined with a tool that is correct (code verifiers, interactive theore provers), then we can get back a correct pipeline.
smellybigbelly 2y ago
One vision in the article that stood out for me, was how formal proof assistants allow for large teams to collaborate on proving theorems. Imagine what we could achieve if we could do mathematics as a hive mind!
- KuriousCat 2y ago
  Reminded me these attempts: https://polymathprojects.org/ https://polymathprojects.org/
- psychoslave 2y ago
  But that's basically what mathematics has been from day 0. What you mention as a hive mind presumably don't refer to a situation where individual minds and intimate reflection can be put out of the equation. On the other hand, mathematics are not possible outside a society which provides a large set of conveniences to leverage on, including communication tools such as a language.
DEEP-MELTDOWN 2y ago
[dead]
benreesman 2y ago
With all respect to luminaries: this will not stand up. This will be treated harshly by history. I’m nobody but I’m going to stand up to Terence Tao and Scott Aarinson: you’re wrong or bought or both. This is a detour and I want to make clear to history what side I was on.
- aamar 2y ago
  What’s your reasoning? There’s much more honor in being right for the right reason than for a wrong one.
  - benreesman 2y ago
    I’m wagering my entire reputation that no LLM, nor any LLM run in a loop, will ever be as intelligent as a precocious child. The burden rests on OpenAI and the scholars on their payroll to show otherwise.
    - benreesman 2y ago
      I have a great many regrets in life but if I died opposing Sam Altman and Fidji Simo and Larry Summers in the newest version of their oppressive lies that would be a good death.
      - kubb 2y ago
        Respect.
    - deleted 2y ago
      [deleted]
    - gbnwl 2y ago
      This isn't really a meaningful prediction unless you define clearly your idea of what being "as intelligent as a precocious child" is, and how you would assess an LLM or any other system against that metric. Though I suppose you avoid the risk of having to move the goalposts later if you never set them up in the first place.
kartwna 2y ago
"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the text." Tao is one of the few mathematicians who is constantly singing the praises of specifically ChatGPT and now CoPilot. He does not appear to have any issues that his thought processes are logged by servers owned by a multi-billion dollar company. He never mentions copyright or social issues. He never mentions results other than "writing LaTeX is easier". Does he have any incentive for promoting OpenAI?
- jstummbillig 2y ago
  Sure: Supporting stuff furthers that stuff. If it works for you, there's your incentive.
  - rthanb 2y ago
    Sure, have a Pepsi. It is delicious! At this stage Tao should disclose whether he has any financial relationship with OpenAI, including stock ownership or even access to experimental models or more computational power than the average user. I've never seen any academic hyping up a company like that, unless they explicitly have/had a financial relationship like Scott Aaronson.
    - deleted 2y ago
      [deleted]
    - JonChesterfield 2y ago
      A decent fraction of this website is people enthusiastically promoting tools they love using. Good tech wins supporters without paying for them.
- screye 2y ago
  Tenured professors are at no risk of losing jobs and have minimum business interests. The literal smartest person in the world will be the last person to lose his job anyway. AI anxiety comes from a fear that AI will replace us, individuals or corporate entities alike. Tao is immune to these risks.
simplemathmind 2y ago
I did not read the pdf, but I think that LLM and Lean could be useful tools for mathematiceans to prove or refute theorems, but the creative idea that sparks knowledge and new theorems lies in the human, the others are tools that can help to reduce time and effort needed and so, indirectly, they can foster and enhance creativity. It also could mitigate some reasoning that require mechanical prove of many details. Anyway, what I just said seems simple and clear, and in no way would it be worth to be published in a high ranking math journal.
- generationP 2y ago
  Right, and the paper you didn't read contains a lot more than that.
  - simplemathmind 2y ago
    I apologize in that case, can you give a brief summary of what is the most important point of that pdf?, I don't know why but my gut feeling is to refuse to read something just based on people reputation. I know that Tao is a very bright mathematician but I also think that he doesn't know much about computer science or computer languages (my evidence is very slim here: once I noted that Tao was very happy with a very simple program, a trivial one, so I inferred from that he still has to learn a lot about programming). For now, it seems clear that the best he can do (for him and us) is to devote his time to math that is his best skill. But it could happen that he could use his best world IQ and math skills to learn how to use LLMs and Lean in a never seem before way to obtain something really valuable. Today I don't think there is any evidence that such thing is going to happen. On one hand, in general, intelligent people are the first to learn how to use new tools in new or better ways, tools that are useful for what they are good at and are devote at. On the other hand, following that path detracts energy from the core of math that requires intuition and creativity and not so much mechanical proofs. On a third hand, there is always the money question that we can not see, that is because is in the third hand.
    - deleted 2y ago
      [deleted]
DominikPeters 2y ago
There are also several videos of Tao giving 1hr talks on this topic, for example https://youtu.be/e049IoFBnLA?t=89 https://youtu.be/e049IoFBnLA?t=89
vouaobrasil 2y ago
I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same thing has happened in chess, with more people advocating for Fischer random because of the boring aspect of preparing openings with a computer, and studying games with a computer. Of course, the computer didn't initiate the process of in-depth opening preparation but it launched it to the next level. The point is that mechanization is boring except for pure utility. My point is that math as a thing of beauty is becoming mechanized and it will lead to the same level of apathy in math amongst the potentially interested. Of course, now it's exciting because it's still the wild west and there are things to figure out, but what of the future? Using advanced AI in math is a mistake in my opinion. The search for truth as a human endeavor is inspiring. The production of truth in an industrialized fashion is boring.
- brap 2y ago
  Human chess players are still incredibly valuable because we want to see what humans are capable of. For the same reason athletes are valuable even though a car can outrun them. With mathematicians, and others working in intelligence-intensive tasks (most of us here probably), I’m not sure what the value would be post-AGI.
  - vouaobrasil 2y ago
    The point is that even with mathematics and programming, there is an underlying community aspect that cannot be ignored, but is hidden under layers of utility. For example, even in programming, people getting together to code, collaborating, and sharing their projects is a small but significant drop in people creating a community. With mathematics, the sharing of ideas and slaving over the proof of a theorem brings meaning to lives by forging friendships. Same with any intellectual discipline: before generative AI, all the art around us was primarily from human minds and were echoes of other people through society. Post-AGI, we abandon that sense of community in exchange for pure utility, a sort of final stage of human mechanization that rejects the very idea of community.
fastneutron 2y ago
The idea of neurosymbolic systems has been in the air a long time, but every time I look at the commentary of an article like this I’m surprised at number the “OMG why didn’t anyone think of this?” type of comments. For a while I got the impression that an ideological undercurrent of “DL vs GOFAI” had gotten in the way of more widespread exploration of these ideas. Tao’s writing here changed my view to something more pragmatic, that being the formalization of the symbolic part of neurosymbolic AI requires too much manual intervention to easily scale. He is likely onto something by having an LLM in the loop with another system like Lean or Athena to iterate on the formalization process.
sylware 2y ago
LLM is probably not the right model for AIs strapped to a formal solver. But experience which has been gained with LLMs may help design those maths oriented models.
deleted 2y ago
[deleted]
riku_iki 2y ago
I know this guy is Fields medalist, but all his recent posts and now this publication lack any substance and actual contributions, so it sounds like he is more in the role of hyped twitter influencer than researcher.

199 points by jalcazar 2y ago

I'd call this paper a "big deal" in that it is a normalization of, very fair summary of, and indication that there is a future for, LLMs in pure mathematics from one of its leading practitioners. On HN here, we've spent the last few years talking and thinking a lot about LLMs, so the paper might not include much that would be surprising to math-curious HN'ers. However, there is a large cohort of research mathematicians out there that likely doesn't know much about modern AI; Terence is saying there's a little utility in last-gen models (GPT-4), and he expects a lot of utility out of combining next-gen models with Lean. Again, not surprising if you read his blog, but I think publishing a full paper in AMS is a pretty important moment.

voxl 2y ago
LLMs as they are I postulate would not work well for this. But, purpose built stochastic auto complete with a type checker to reject the junk? That could be actually useful. Funnily enough it's also a domain of application that wouldn't make any money at all. It would have to be an offline LLM that is reasonably efficient to execute locally.
- xaml 2y ago
  Why would it not make any money?
deleted 2y ago
[deleted]
Syzygies 2y ago
Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible. I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to explain so we can generalize? Machine proofs tend to be inscrutable. While "the singularity" is unlikely anytime soon, we should recall that before the first atomic test there were calculations to insure that we didn't ignite the atmosphere. We're going to need proofs that we have control of AI, and there's an obvious conflict of interest in trusting AI's say so here. We need to understand these proofs.
- nextos 2y ago
  This is also my take on this. IMHO, LLMs + theorem provers have the potential to make formal methods cheap enough to use more widely. And we should give more credit to the theorem prover part of the equation, which comes in part from old AI symbolic efforts.
- vessenes 2y ago
  Interesting thoughts, thanks. It seems to me a model trained to generate Lean could also be purposed to explain a large Lean proof, and that’s very interesting. So much of modern math is limited to extremely small cohorts. None of that is dispositive inre provable safety, obviously.
- rowanG077 2y ago
  A good thing about machine proofs is that, just like code, they can be refactored. I also use LLMs when writing code, but the code that I end up pushing is almost never exactly what the LLM has generated. I don't really see the problem with that. It's way less taxing for me mentally to get an LLM to generate definition and implementations and just refactor them quickly. I would expect LLMs for lean to be similar in the future.

jfmc 2y ago

Actually, most of the paper seems a bit obvious from the computer science side. LLMs scale for really complex tasks, but they are neither correct nor complete. If combined with a tool that is correct (code verifiers, interactive theore provers), then we can get back a correct pipeline.

smellybigbelly 2y ago

One vision in the article that stood out for me, was how formal proof assistants allow for large teams to collaborate on proving theorems. Imagine what we could achieve if we could do mathematics as a hive mind!

KuriousCat 2y ago
Reminded me these attempts: https://polymathprojects.org/ https://polymathprojects.org/
psychoslave 2y ago
But that's basically what mathematics has been from day 0. What you mention as a hive mind presumably don't refer to a situation where individual minds and intimate reflection can be put out of the equation. On the other hand, mathematics are not possible outside a society which provides a large set of conveniences to leverage on, including communication tools such as a language.

DEEP-MELTDOWN 2y ago

[dead]

benreesman 2y ago

With all respect to luminaries: this will not stand up. This will be treated harshly by history. I’m nobody but I’m going to stand up to Terence Tao and Scott Aarinson: you’re wrong or bought or both. This is a detour and I want to make clear to history what side I was on.

aamar 2y ago
What’s your reasoning? There’s much more honor in being right for the right reason than for a wrong one.
- benreesman 2y ago
  I’m wagering my entire reputation that no LLM, nor any LLM run in a loop, will ever be as intelligent as a precocious child. The burden rests on OpenAI and the scholars on their payroll to show otherwise.
  - benreesman 2y ago
    I have a great many regrets in life but if I died opposing Sam Altman and Fidji Simo and Larry Summers in the newest version of their oppressive lies that would be a good death.
    - kubb 2y ago
      Respect.
  - deleted 2y ago
    [deleted]
  - gbnwl 2y ago
    This isn't really a meaningful prediction unless you define clearly your idea of what being "as intelligent as a precocious child" is, and how you would assess an LLM or any other system against that metric. Though I suppose you avoid the risk of having to move the goalposts later if you never set them up in the first place.

kartwna 2y ago

"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the text." Tao is one of the few mathematicians who is constantly singing the praises of specifically ChatGPT and now CoPilot. He does not appear to have any issues that his thought processes are logged by servers owned by a multi-billion dollar company. He never mentions copyright or social issues. He never mentions results other than "writing LaTeX is easier". Does he have any incentive for promoting OpenAI?

jstummbillig 2y ago
Sure: Supporting stuff furthers that stuff. If it works for you, there's your incentive.
- rthanb 2y ago
  Sure, have a Pepsi. It is delicious! At this stage Tao should disclose whether he has any financial relationship with OpenAI, including stock ownership or even access to experimental models or more computational power than the average user. I've never seen any academic hyping up a company like that, unless they explicitly have/had a financial relationship like Scott Aaronson.
  - deleted 2y ago
    [deleted]
  - JonChesterfield 2y ago
    A decent fraction of this website is people enthusiastically promoting tools they love using. Good tech wins supporters without paying for them.
screye 2y ago
Tenured professors are at no risk of losing jobs and have minimum business interests. The literal smartest person in the world will be the last person to lose his job anyway. AI anxiety comes from a fear that AI will replace us, individuals or corporate entities alike. Tao is immune to these risks.

simplemathmind 2y ago

I did not read the pdf, but I think that LLM and Lean could be useful tools for mathematiceans to prove or refute theorems, but the creative idea that sparks knowledge and new theorems lies in the human, the others are tools that can help to reduce time and effort needed and so, indirectly, they can foster and enhance creativity. It also could mitigate some reasoning that require mechanical prove of many details. Anyway, what I just said seems simple and clear, and in no way would it be worth to be published in a high ranking math journal.

generationP 2y ago
Right, and the paper you didn't read contains a lot more than that.
- simplemathmind 2y ago
  I apologize in that case, can you give a brief summary of what is the most important point of that pdf?, I don't know why but my gut feeling is to refuse to read something just based on people reputation. I know that Tao is a very bright mathematician but I also think that he doesn't know much about computer science or computer languages (my evidence is very slim here: once I noted that Tao was very happy with a very simple program, a trivial one, so I inferred from that he still has to learn a lot about programming). For now, it seems clear that the best he can do (for him and us) is to devote his time to math that is his best skill. But it could happen that he could use his best world IQ and math skills to learn how to use LLMs and Lean in a never seem before way to obtain something really valuable. Today I don't think there is any evidence that such thing is going to happen. On one hand, in general, intelligent people are the first to learn how to use new tools in new or better ways, tools that are useful for what they are good at and are devote at. On the other hand, following that path detracts energy from the core of math that requires intuition and creativity and not so much mechanical proofs. On a third hand, there is always the money question that we can not see, that is because is in the third hand.
  - deleted 2y ago
    [deleted]

DominikPeters 2y ago

There are also several videos of Tao giving 1hr talks on this topic, for example https://youtu.be/e049IoFBnLA?t=89 https://youtu.be/e049IoFBnLA?t=89

vouaobrasil 2y ago

I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same thing has happened in chess, with more people advocating for Fischer random because of the boring aspect of preparing openings with a computer, and studying games with a computer. Of course, the computer didn't initiate the process of in-depth opening preparation but it launched it to the next level. The point is that mechanization is boring except for pure utility. My point is that math as a thing of beauty is becoming mechanized and it will lead to the same level of apathy in math amongst the potentially interested. Of course, now it's exciting because it's still the wild west and there are things to figure out, but what of the future? Using advanced AI in math is a mistake in my opinion. The search for truth as a human endeavor is inspiring. The production of truth in an industrialized fashion is boring.

brap 2y ago
Human chess players are still incredibly valuable because we want to see what humans are capable of. For the same reason athletes are valuable even though a car can outrun them. With mathematicians, and others working in intelligence-intensive tasks (most of us here probably), I’m not sure what the value would be post-AGI.
- vouaobrasil 2y ago
  The point is that even with mathematics and programming, there is an underlying community aspect that cannot be ignored, but is hidden under layers of utility. For example, even in programming, people getting together to code, collaborating, and sharing their projects is a small but significant drop in people creating a community. With mathematics, the sharing of ideas and slaving over the proof of a theorem brings meaning to lives by forging friendships. Same with any intellectual discipline: before generative AI, all the art around us was primarily from human minds and were echoes of other people through society. Post-AGI, we abandon that sense of community in exchange for pure utility, a sort of final stage of human mechanization that rejects the very idea of community.

fastneutron 2y ago

The idea of neurosymbolic systems has been in the air a long time, but every time I look at the commentary of an article like this I’m surprised at number the “OMG why didn’t anyone think of this?” type of comments. For a while I got the impression that an ideological undercurrent of “DL vs GOFAI” had gotten in the way of more widespread exploration of these ideas. Tao’s writing here changed my view to something more pragmatic, that being the formalization of the symbolic part of neurosymbolic AI requires too much manual intervention to easily scale. He is likely onto something by having an LLM in the loop with another system like Lean or Athena to iterate on the formalization process.

sylware 2y ago

LLM is probably not the right model for AIs strapped to a formal solver. But experience which has been gained with LLMs may help design those maths oriented models.

deleted 2y ago

[deleted]

riku_iki 2y ago

I know this guy is Fields medalist, but all his recent posts and now this publication lack any substance and actual contributions, so it sounds like he is more in the role of hyped twitter influencer than researcher.