Machine-Assisted Proof [pdf]
ams.org
ams.org
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.
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.
We arrived at engines before online chess, and the two have come up together — both being enabled by the growth of computers. You can choose not to use an engine, but it will exist either way because others will choose to use it when it’s enabled by those same things.
To get rid of the engine, you have to get rid of computers — or in the case of Freestyle/Chess960, create so many openings a human can’t memorize them all so only has a short time to prepare.
And a suspicion and dislike of advanced technology IS growing among people outside the technophile sphere.
Preserving people's access to this kind of enjoyment is not something that should carry any weight in my opinion.
> The product of mathematics is clarity and understanding. Not theorems, by themselves... mathematics only exists in a living community of mathematicians that spreads understanding and breaths life into ideas both old and new. The real satisfaction from mathematics is in learning from others and sharing with others. All of us have clear understanding of a few things and murky concepts of many more. There is no way to run out of ideas in need of clarification. The question of who is the first person to ever set foot on some square meter of land is really secondary. Revolutionary change does matter, but revolutions are few, and they are not self-sustaining --- they depend very heavily on the community of mathematicians.
https://mathoverflow.net/questions/43690/whats-a-mathematici...
Ongoing relationships and cooperation is how humanity does its peak stuff and reaches peak understanding (and how humans usually find the most personal satisfaction).
LLMs are powerful precisely because they're a technology for concentrating and amplifying some aspects of cooperative information sharing. But we also sometimes let our tools isolate.
Something as simple as a map of a library is an interesting case: it is a form of toolified cooperation, you can use it to orient yourself in discovering and orienting library materials without having to talk to a librarian, which saves time/attention... and also reduces social surface area for incidental connection and cooperation.
That's a mild example with very mild consequences and only needs mild individual or cultural tools in order to address the tradeoffs. We might also consider markets and the social technology of business which have resorted in a kind of target-maximizing AGI. The effects here are also mixed, certainly in terms of connection / isolation, also potentially in terms of environmental impact. A paperclip maximizer has nothing on an AGI/business that benefits from mass deforestation, and we created that kind of thing hundreds of years ago.
The question is if we're going to maintain the kind of social/cultural infrastructure that could help us be aware of and continue to invest in the value the social/cultural infrastructure.
Or, put more simply, if we're going to build a future for people.
To be clear I don’t think AI is bad, and even if it is I’m pretty damn sure it’s not avoidable. But we’re in for drastic changes and we should start getting used to it.
I think we have to do both: get used to it, but fight it at the same time in case we can get rid of it.
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.
Yes, a few people might find some meaning in a life where they are not that important, but most people need to feel important to others, and AI takes that away.
This is partly why I think that the pace of AI development needs to slow down. We've had disruptive technologies in the past, and society eventually adapted when new jobs were created, but none of them had the potential to completely replace humans in most industries. None of them raised existential questions about our humanity, the value of human labor, our place in society, and the core pillars of economy, education, etc. And, crucially, none of them were developed in just a few years.
We need time to discuss these topics and prepare for the shift. But, of course, any mention of slowing down is met with criticism of regulations stifling innovation and profits, concern about losing a technological advantage over political opponents, etc., so this is unlikely to happen.
This century certainly won't be boring, so let's enjoy the ride, and hope that no major conflict pops off. Though with the way things are going, my hope is waning.
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.
We’re past the point of just going back to preindustrial tech with less negative impacts- but with a deeper understanding of reality we could, e.g. pull carbon straight out of the atmosphere to manufacture almost anything in a renewable way, while also understanding biochemistry enough to make things that won’t be toxic or persist in the environment, and are readily broken down and reused.
This is where we fundamentally disagree. I don't believe (and I've never seen any convincing evidence) that we could EVER develop more human and environmentally safe technology. Primarily because technology always requires physical resources (mining) and habitat destruction, and because there are 8 billion people in the world and there will always be the unscrupulous who will use that technology for destruction. And even ignoring the unscrupulous, the existing habitat destruction from said technology use already (in my valuation) is too great to balance out some of the so-called positive uses of technology.
There is no fundamental reason to require such things. As Fuller said, the goal of technology is to “do more and more with less and less until you can do everything with nothing.”
In my view it’s not the idea of technology that has been the problem, but that it was done by people with no understanding of the impacts, or sense of responsibility. The reason our current tech is so nasty and damaging is because our knowledge has been too primitive to do better thus far, and now people are not willing to give it up.
Synthetic biology, for example can now pull carbon straight from the air and make it into nontoxic biodegradable building materials- or really almost anything. This can eventually replace all mining and toxic chemical factories, with basically just old fashioned fermentation in a vat, that neither produces or uses anything toxic- but can replace all of the nasty stuff we currently make from mining and petroleum. A deeper understanding of biology will allow us to further reduce risks and environmental impacts by really deeply understanding which molecules we can make safely without toxic impacts on humans or other species, and without environmental persistence.
It all comes down to probabilities, but when people find a more efficient way to use something, they use more of it.
Is there a nonzero probability that your closed economoy, zero-mining future is possible? I think so, but I think it's small. And even a 10% chance that your future will NOT come to pass is enough reason to limit technology and go for degrowth instead, which seems far more logical.
No doubt that our differences will ultimately come to valuations and what we consider important, not probabilities. There will be no reconciliation there.
Of course, what I am saying is probably entirely moot, because economy and science as it is today favors your position, and not mine. But I am willing to fight for my position regardless.
However, there is more than a small chance of the future I am talking about being possible where we can make virtually anything directly from carbon in the air, with little to no impacts. I am an academic scientist, and am focused on solving the specific problems that will make what I am talking about possible- and basically everything I mentioned is already working fairly well... and is already cheaper, safer, and more practical then petroleum chemistry and mining if you factor in externalities. However, the only real path I see to getting people to use it is to make it better still, so it is fundamentally cheaper and superior, without even factoring in the externalities and nasty impacts of our current way of doing things.
Degrowth is quite frankly not going to happen voluntarily, it's a cultural and political non-starter, and also leaves us with an inability to fix the massive damage to the planet we've already caused, and leaves us dying from diseases that we are very close to understanding how to prevent. We've decimated and poisoned our natural environment such that simple living is no longer even possible in most places- where I live the fish and other wildlife are almost all gone, and the few left are too toxic to eat. Let's instead go all in on understanding science so that we can in principle do almost anything we can imagine with little resources or impacts, and then also have much higher standards for what we actually choose to do with the knowledge.
Edit: I looked at your blog and agree with a lot of what you are saying, but also disagree with a lot, but see you are a deep thinker that cares a lot about this stuff. I think it would be interesting to talk to you more.
I really would like a citation for this, perhaps several. How do we make various metals from carbon from the air? How could we make the silicon for the solar panels? Lubricants for the wind turbines? Lithium for the batteries? Or will all batteries be made out of pure carbon?
Metal is required for industrial civilization. Even if it isn't, not everything could be made from just the gaseous elements in the air.
I really do love the idea that we COULD do that. If you're right, what I am doing is completely unnecessary. In that case, I will gladly accept that I am wrong.
But if I am right, then civilization will start to destabilize and we will have to give up advanced technology and I will also accept that and work towards making that a better future.
I may not be right all the time, and honestly, TRULY, hope that I am wrong....feel free to email of course if you ever want a deeper chat.
Basically, replace most electricity with photonics, the rest with ionics. We have efficient ion-flow based computing and flying machines, don't we? (Birds & brains)
As for how to revamp the rest of the "irreplaceable" material culture not based on photosynthesis: What's in it for me to talk to you about this :)? How many years further have you seen than Grothendieck, since Fuller was not so visionary after all? (Including, how to fund actionable, scalable stuff, that's 30 years give or take 5)
(Note that there are siliceous, if not entirely silicon-based, lifeforms on earth. Diatoms, molluscs, etc, perhaps a significant amount of our low-end chips already come from them, through seasand? :)
With precise, programmable control over biochemistry, we can make almost any organic carbon based molecule from almost any other carbon source- but obviously not things like metals. However, I posit we will be able to make things with drastically superior performance that fills all of the same use cases. Consider for example that Dyneema - which is just simple straight saturated carbon chains- is already 15x the strength of steel on a weight basis. I'm talking about being able to predict the properties of a molecule ahead of time, and then make something with exactly the properties we want.
It would be quite shortsighted to make a more environmentally friendly way of making the exact same stuff when those things were limited by constraints that no longer apply and we have the potential for drastically superior materials (stronger, more durable, lower toxicity, more recyclable, etc.) for a specific problem- but it depends on what specific problem you are addressing.
FWIW I doubt we understand biology enough today to make biomanufacturing more efficient than conventional industrial processes, see the non sequitur of fungi based meat substitutes.
However, in the meantime, we can defo learn from bio to improve or even revolutionize our processes.
The other thing is: CO2 capture is also going to be far less feasible than increasing albedo, that's where we should focus our short term imagination. Don't lose hope for albedo increase to be biotech based, in the short term, though!
(Eat meat that shit little yet fart more like humans)
You can start easier today (thanks thoughtful USian industry!) from, otc https://www.himedialabs.com/us/m643a-mineral-modified-glutam...
Following, e.g. (thanks academia!) https://www.researchgate.net/publication/46007644_Enhancemen...
Also note they are better thought of as anaerobic.
Also diyrs, if you're to wean off the Man, keep detailed notes (or at least back up your pdfs on tape)!
Source: have tried basic MSGM "at home" for easier anaerobes, reasonably successful
Found this, also seems diyable, not chips, but li batt anodes from beachsand (thanks the lowest end of springer-demia!) https://www.nature.com/articles/srep05623
Come on now. Renewable energy is gaining on fossil fuels around the world. The air in London used to be thick with smog, and now it's not. Acid rain is a thing of the past. The ozone hole is shrinking.
Fire and the wheel are technology; are you against them too?
What matters to me is CO2. When we can drop that below 400, then I will be impressed. As for now, I'm waiting to see if this is not just a case of Jevon's paradox.
> Fire and the wheel are technology; are you against them too?
No, those are local technologies that anyone can make with some basic knowledge. I am not against primitive technologies. We will always use them. What I am saying is that we should be like the Amish: examine individual technologies for their long-term consequences, and not develop those. And, we should regress many as well. The discussion of which and how would be lengthy but we should have it (as a society).
However, I do wonder if they are still able to make coherent decisions about the net benefits of various technologies, without a deep level of technical and scientific training nowadays. Living up against a world of people not making the same choices as them would present a lot of new challenges- for example, if a chemical factory is placed nearby... are they learning how to use mass spec to see if they are being poisoned? Or to read scientific literature to see what the likely risks and impacts of that poisoning is? Sure they could hire external experts, but can they trust people that don't share their views and values to navigate those issues as they would?
Taking personal responsibility for if a technology is appropriate to use or not may require an even deeper level of technical and scientific knowledge than the usual approach of not being critical of technology.
Sure they can fold space-time and have quantum computers the size of dust particles, but they also use traditional tools from their ancient history when appropriate or when it serves a role in their culture. They also don’t do absolutely everything they know how to do, deciding some things are harmful or useless.
You see this sometimes in sci-fi, e.g. Star Trek.
It’d probably be a sign of being advanced far beyond the hype phase, even having gone through many hype - disillusionment - enlightenment phases. They would be far post the phase where things look like cyberpunk, but you’d probably see phases like that in their history.
When it comes to making decisions, I am pretty sure no one in modern society makes any choices when it comes to the net benefits, only the short-term gains. That's regardless of how much technical training they have. And the net benefits are mainly about the use, not how the thing works, so people could really indeed make such decisions if there were a governing body to do so.
I really don't think you realize how cushy modern life is compared to even the hardships of a few hundreds years ago.
A fair argument as far as it goes, but unlike engineering and some other activities, mathematics isn't about creating more technology. Although mathematics can be applied to that purpose, that's not its essence.
If electronics and computers didn't exist, if industrial society didn't exist, mathematics would still exist, and perhaps it wouldn't be confused so often with its applications.
Mathematics isn't responsible for how we choose to apply it.
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.
You’re lamenting that inventing boats has destroyed the beauty of swimming.
- - - Edit - - -
Responding to your expanded argument:
You could never swim to a new continent, which boats enabled. This is the same — people can choose to keep doing the same limited math themselves, in a slower way, but will never reach the places people can aided by tools. That’s simply how the world is. But we shouldn’t restrict the distance people can travel to adhere to the aesthetics of swimming.
You’re arguing precisely that: we must limit our intellectual journey because you don’t approve of the aesthetics of the tool to travel further.
But you’ve subtly changed your argument: before you were arguing that the beauty was in creating mathematics, not merely learning already written mathematics.
My exact point is that learning surmathematics (math taken further by AI) is it’s own interesting pursuit — and appeals to my sense of aesthetics and adventure more than piddling around merely to say it was all done by human hands.
I’m not following where you believe the swimming and boat analogy breaks down: there’s still the same personal reasons to learn and do mathematics one might swim; but learning surmathematics is an adventure to a whole new land.
- - - Edit - - -
Responding to sibling comment as well:
> I am arguing that we should limit our intellectual journey, to preserve the humanistic aspects of the journey. That is exactly my position.
That’s exactly what I compared to swimming rather than boats — because you won’t reach the same places and it’s done for aesthetic reasons.
Some people (eg, myself) want the surmathematics adventure.
For some reason, and I can't explain it, but I do believe that people still value personal physical achievements even when machines can do it better, but the same is not true of mental achievements. I take it as an axiom.
> Some people (eg, myself) want the surmathematics adventure.
That is where we fundamnetally differ, again axiomatically. I think it's offensive. But even if you do like it, that will eventually lead to the path where AI is just doing mathematics so well that no one will have much of a chance to understand what it is doing at all. And that ultimate conclusion, or even a probably chance of it, is enough reason to scrap the whole thing.
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.
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.
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.
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.
LLMs are way more useful than a child in many ways, some of which are discussed in the article. They don't need to be as intelligent as a child for anything proposed in the article.
A flaw in the Turing test is failing to specify which person is making the judgement. We're working with statistical distributions here and I would not bet on the intellect displayed by the LLM models being below that displayed by the human population today, let alone with more improvement to one or degradation to the other.
More concretely, if you sketch some normal distributions on a whiteboard for people vs machine based on how you see things, it should be hard to confidently claim minimal overlap.
Are LLMs useful enough? I don't know.
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.
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?
And there are a lot of us.
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?
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.
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.
There's quite a few solutions to choose with per-request pricing. Only extremely heavy users should be on the subscription these days.
You can invest in running things yourself too.
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.
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.
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.