Machine-Assisted Proof [pdf]

I&#x27;d call this paper a &quot;big deal&quot; 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.<p>On HN here, we&#x27;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&#x27;ers. However, there is a large cohort of research mathematicians out there that likely doesn&#x27;t know much about modern AI; Terence is saying there&#x27;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.<p>Again, not surprising if you read his blog, but I think publishing a full paper in AMS is a pretty important moment.

There are also several videos of Tao giving 1hr talks on this topic, for example <a href="https:&#x2F;&#x2F;youtu.be&#x2F;e049IoFBnLA?t=89" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;e049IoFBnLA?t=89</a>

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.<p>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.<p>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&#x27;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.<p>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&#x27;s exciting because it&#x27;s still the wild west and there are things to figure out, but what of the future?<p>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.

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.

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!

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

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.

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.

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

&quot;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.&quot;<p>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.<p>He never mentions copyright or social issues. He never mentions results other than &quot;writing LaTeX is easier&quot;.<p>Does he have any incentive for promoting OpenAI?

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.