Machine-Assisted Proof [pdf]
ams.org
Machine-Assisted Proof [pdf]
1–10 of 106 posts
Re: Machine-Assisted Proof [pdf]
#2I'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.
Re: Machine-Assisted Proof [pdf]
#3Actually, 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.
Re: Machine-Assisted Proof [pdf]
#4One 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!
Re: Machine-Assisted Proof [pdf]
#5I'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 mathematicia…
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.
Re: Machine-Assisted Proof [pdf]
#6[dead]
Re: Machine-Assisted Proof [pdf]
#7One 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!
Reminded me these attempts: https://polymathprojects.org/
Re: Machine-Assisted Proof [pdf]
#8One 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!
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.
Re: Machine-Assisted Proof [pdf]
#9With 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.
Re: Machine-Assisted Proof [pdf]
#10"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?