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.
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.
And we should give more credit to the theorem prover part of the equation, which comes in part from old AI symbolic efforts.
None of that is dispositive inre provable safety, obviously.
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.
Chess is a game, if it gets boring that defeats the point…. Math on the other hand is basic science research, and enables us to understand how the universe and our bodies work, to massive benefit. I don’t care how “boring” it is, the knowledge could have immense value or be critical for our survival and if AI can allow us to access it, all the better.
While you might be right, it is VERY far from clear that the latest advanced research will really help us. It could also lead to our annihilation or at least dehumanization, which is really not much better than annihilation.
In fact, due to the immense damage technology has caused, the burden of proof should be on the technologists to reliably demonstrate that new technology is even worth it beyond propping up our broken, global capitalistic system.
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.
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.
It wouldn't be much different from small artisan shops we have today in other industries. Mass production will always be more profitable, but there's a market for products built on smaller scales with care and quality in mind. Large companies that leverage AI black boxes won't have that attention to detail.
I too feel saddened by the idea of automating math if it leads to inscrutable proofs or theories. But it seems essential that we advance the tools used for mathematical discovery if we hope to keep advancing. Hopefully we can find a balance where the advancement of mathematical understanding continues to be a human story, but we're not artificially held back by pretending new tools don't exist.
Nobody examines structure of group diagrams because drawing interesting ones by hand is borderline impossible, but takes just a few minutes on a computer. However, they’re a natural way to arrive at algebraic/geometric equivalence. (And indeed, the first time I had an intuition for it.)
To me, you sound like someone lamenting swimming is meaningless because we invented boats.
There is also a fundamental difference between swimming and math. There is no prisoner's dilemma situation when it comes to swimming: with swimming, people CHOOSE to swim because they like it. But due to different incentives, people will CHOOSE to use AI only because others use it and it will become the only path eventually.
In other words, swimming is still possible even though boats exist. People going into mathematics will not have the possibility of being of any use without AI, because the prisoner's dilemma (arms race) will ensure that math is no longer about anyone caring about math without AI.
It's the same difference between "dumb" algorithms and "generative AI" algorithms. The generative AI has the capability to replace human thinking in some cases, whereas the dumb algorithms only replace rote work. Since creativity is not just what allows innovation but also forms the center of community and personal expression, we are also replacing those "soft" components of scentific exploration that eliminate the importance of the individual.
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’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.
https://mathstodon.xyz/@tao/113132502735585408
It may only take one or two further iterations of improved capability (and integration with other tools, such as computer algebra packages and proof assistants) until the level of "(static simulation of a) competent graduate student" is reached, at which point I could see this tool being of significant use in research level tasks.
And there are a lot of us.
I’m calling bullshit on AGI. I’m repudiating as offensive both the ill intentions and the technical failure of these people.
I’m proposing that all sincere hackers denounce OpenAI as a matter of principle.
Did I stutter?
There’s much more honor in being right for the right reason than for a wrong one.
The burden rests on OpenAI and the scholars on their payroll to show otherwise.
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?
His job is publishing his thoughts. They're not going to a single company, but everyone. If he gets results faster, we all get to see his thought process faster. Ideally, chatgpt would be familiar with everything coming from researchers like him.
> constantly singing the praises of specifically ChatGPT and now CoPilot
Chatgpt is mentioned just once and only as a "such as" example.
Everything from IDEs to Google search gets the same treatment.
I remember a colleague watching me edit code exclaiming that I was "Cheating!" because I had syntax highlighting and tab-completion.
Another coworker who had just failed to get answers after searching for "My PC crashed, how to fix?" kept telling me that the results "couldn't be trusted". He was reading Windows XP bug reports over a decade out-of-date for troubleshooting a Windows Server 2022 issue that manifests only on Azure.
Some people are afraid of these things and suspect there's a hidden agenda, others see things for what they are: Just tools, each fit for a particular purpose.
My experience is exactly the opposite: Inept power users jump on the latest bandwagon to camouflage their incompetence. And like true power users they evangelize their latest toy whenever they can.
Well, there's also the arms-race scenario. A classic example is computer security: people only make computers more secure because people hack them, which makes hackers improve their stuff. This prisoner's dilemma scenario gives a deterministic force to technology that certainly makes it more than just a tool: it is a force that acts upon society that transcends human choice.
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.
AI anxiety comes from a fear that AI will replace us, individuals or corporate entities alike. Tao is immune to these risks.
https://meta.mathoverflow.net/questions/6039/has-mo-been-red...
The question of exploitation is not a question of anxiety, but of exasperation.
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.
