Mathematics in the age of AI(arxiv.org) |
Mathematics in the age of AI(arxiv.org) |
> My own suggested rule of thumb: if the authors cannot convincingly demonstrate that they are able to give a clear, expert-level talk on their results, one that is correct and properly attributed, then the result should not be published. A proof that no human can properly explain should be viewed as incomplete, even if it has been formally verified.
I think these are non-trivial epistemology and science theory problems.
Tao is essentially saying that the only value in a proof is its ability to be understood, but that's wrong. A proof is also valuable because it establishes a new fact. The fact is useful in itself, even absent an explanation.
From a different angle, what we don't understand can absolutely hurt us and you're right too, but it doesn't contradict Tao's viewpoint.
Edit: if you had a PoC cracking the encryption, I think the result is still publishable due to impact and the fact of the empirical result. That's different from some esoteric proof that nobody is even sure it's right.
> Let's say tomorrow someone comes up with a formally verified proof that a major encryption algorithm underpinning the security of the internet can be trivially broken, but they can't explain it. You're saying it should be kept under wraps and not published?
Absolutely. It could also be exploiting bugs in the verifier. Even if not -- even if that proof were correct and entirely written by humans, care should still be taken in how such knowledge is published. I'd want to give trusted parties a chance to try to fix the issue before letting it be known by black-hats, for instance.
I'm deeply suspicious. I do not yet have a concise statement for why, but a lot of literature on the sociology of knowledge work sort of points at my thoughts.
Section 5 of the Thurston article cited by Tao touches the elephant. Raduchel's article on the economics of software [2] also touches it.
I've tried to put words to this for a few years. I think I'm just going to start writing versions of it as see if that helps me shape the thought into something more concise.
So, in the spirit of this article's style, here are some postulates:
1. There is a sociological process happening in the production function during knowledge work.
2. That production function and the associated sociological process spans years or even decades, and must outlast many of the artifacts that are produced during the early years of the function.
3. You cannot get the right lines of code or the right theorems proved without running that sociological process alongside the artifact production process.
4. It is impossible to completely separate the sociological process from the artifact construction process. If you just iterate on artifacts then too much of the required hidden state is lost to make progress in the right direction. This is true even if you include distilled artifacts capturing pieces of the sociological process (eg meeting notes, documentation, commit logs, prompts).
5. So you need that sociological process, or something like it, to still happen.
6. For a lot of knowledge work that process plays out in extremely high-fidelity social interactions [3] that we have not yet captured in the datasets that would be required to reproduce those dynamics.
7. And even if we do collect that data, our current architectures and training algorithms and hardware would be useless given the size of the datasets.
So: the technology today gives us the ability to iterate on the production of artifacts. But it does not sufficiently simulate the social process which gives rise to the Right artifacts.
This isn't exactly what I actually think, but it's a version of the thing that I intuit when I watch heavy use of AI in both software projects and formalization projects. And simulating that process feels way harder than people are currently assuming.
[1] https://arxiv.org/pdf/math/9404236 Section 5.
[2] https://www.nationalacademies.org/read/11587/chapter/11 pp 166-168.
[3] there is a reason we still gather in-person around white boards, and why doing so is more crucial for some types of work than others.
Properly explain is an enormous grey area. Soon, I think, there will be proofs of results that are verified in Lean that are so long that no one will be able to “properly explain”. I don’t think they should be discarded.
Resolution of singularities is a famous theorem of Hironaka. Abhyankar claimed that no one truly understood the proof of the theorem. He said that he and Zariski couldn’t get through the paper with a full understanding. But everyone accepts this theorem as being correct.
Hmm, doesn't it take an expert to explain why those cases are exhaustive, and why the code that checked them is correct?
Tangentially, I'm not a mathematician but I wonder if one "opaque" proof that is too complicated for anyone to understand, but that we know is correct via formal verification, might end up being built on with "transparent" human-understandable proofs. For example, it's my understanding that there are many conjectures that have been proven true conditional on the riemann hypothesis being true. In that case, an opaque proof of the riemann hypothesis would enable those conjectures to be known and built upon
Just burn lots of tokens on the frontier model of your choice to let the AI find a high-level argument why the four color theorem holds. :-)
--
Seriously: since there exist quite a lot of readers on HN who are both hardcore into AI and mathematical problems: This is a challenge for you.
I am looking forward to seeing an announcement of a novel high-level argument why the four color theorem holds on the first page of HN in at most a month. :-D
For many of the rest of us, mere consumers of mathematical results, it’s sufficient to know that a^2 + b^2 = c^2 was proven by somebody or some machine at some point.
It would work better as a bar for hiring, rather than as a bar for publishing.
I am probably being too optimistic, but wouldn't it solve the problem if peer-review had a pre-screening phase where you give a presentation about your work? Similarly to how a PhD presentation is given. It could give back the publishing power to the expert, rather than the journals.
Once you have validated that the knowledge you want to publish is yours and that you actually understand and own the work, then it doesn't matter if the paper is written by a LLM or if the LLM assisted you in doing the work.
He's a typical person otherwise, politically aware of how he barters for food; until proven otherwise this can be seen as little more than social moat defense.
To paraphrase a quote attributed to Upton Sinclair; hard to get a worker to understand something when their paycheck relies on them not understanding it.
The only interesting thing here is the frogs high up admitting they feel the heat.
We'll end up with incomprehensible math because comprehensibility isn't rewarded. No one is going to get a Fields Medal, or tenure, for digesting someone else's results.
The incentive will be to be able to publish in a top tier journal. I suspect what Tao is advocating for is having journals reject such manuscripts.
> No one is going to get a Fields Medal, or tenure, for digesting someone else's results.
I'm sure no one gets a Field's Medal if others can't digest their results.
He says it shouldn't be able to published if they can't explain it. Publishing it is the reward.
It should be ignored and refused.
Science,at its core, does not care about the credentials or institutions. It cares about the results and to what extend they can be falsified.
This feel a bit like "we know all about physics, we can only get more precise" - moment
I noticed a long time ago, that the more people focus on trivialities like typos when arguing against someone online, the more compelling the original argument is. Basically, bikeshedding.
The most compelling evidence of the compelling nature of the original argument is when the most-upvoted reply is a joke or a meme. That's when you really know that those responding have nothing else to say. It's a white flag being run up, or the dog turning over and exposing its belly.
Some academic cultures have a tradition of formal debates. They are based on the premise that an educated person should be able to argue convincingly for or against any idea, regardless of whether they believe in it. A natural corollary is that you should not let convincing arguments convince you, as the merits of the argument have little to do with the merits of the idea itself.
LLMs have made the situation worse. People's ability to generate convincing arguments now greatly exceeds their ability to evaluate the value of ideas.
No one talks about why the proof works, but they will happily spend thousands of pages explaining how it works.
If Amazon uses AI math to come up with better routing, the cats can benefit from cheaper delivery fees just as much as humans can. No understanding needed.
The human brain is being obsoleted, soon thinking is going to be a recreational activity like weightlifting. If you want to think as a hobby, that's fine, but most people will be free of that toil of unwanted brain labor.
If a subset of mathematicians, use AI to condense timelines focusing on goal 6.2 exclusively and make rapid progress and reach a proverbial inflection point — one where value proposition of the using this new normal is too enticing to give up — everyone will ask: "This thing is so awesome. Why should I care about your values?"
Understanding was critical for the field to progress when only humans were involved but if humans are not needed to make progress, I wonder if we split into two worlds: an AI math-world where amazing new results continue at a rapid pace bottlenecked only by compute/cost and a human math-world where we understand a subset of the AI math-world as a hobby (similar to Stockfish vs human chess).
I am wary of AI in all aspects I am seeing it in but in many ways in mathematics seems to me the least troubling. It will change things in and the field will not be the same. Blacksmithing has not really gone away. You can still work as a farrier, if you like that sort of things. The tools that replaced a man working over a forge with a big hammer are part of a giant industry that is still producing works for the modern world.
The Busy Beaver game has lead to a better understanding of complexity theory and automata. Also, direct "hands on" work on improving proof assistants and related tools.
Btw, for those who are curious, the Busy Beaver Challenge wiki is a treasure trove of rabbit holes and curiosities:
This is also the strategy I use for editing drafts of my books. I bring a printed draft to someplace nice (e.g. coffee shop or park) and read it all carefully, then I transfer the edits back to the .tex sources. I do several passes of this, until I feel the text + explanations are solid.
Reading on screen just isn't the same...
It's the old cliche of "if you only have a hammer every problem looks like a nail". Let's not fall into the trap of thinking that our life needs to be 100% about AI or completely devoid of AI. We can really use this thing to make our lives better.
Instead of wasting time on the question of whether we should use it, let's focus on HOW we'll use it.
And one thing about Tao: it's really refreshing to have an influential genius "around" who isn't a egomaniacal psychopath trying to rule the world through their XYZ corporation but, instead, being a reasonable and well-balanced person. Big fan.
The only thing to do is to be all in, or get run over.
Ahh. I know Terrence Tao didn't have the following in mind when he said those words, but oh man, the philosophy neurons are firing in my brain rn.
And the term "artificial intelligence (AI)" has been the name of the field for 70 years and counting. If anything, "LLM" is a misnomer that's been lingering around since 2018-19. When the term was coined, these systems were relatively small, experimental, and could only produce impractical facsimiles of the English language. This is obviously no longer the case today.
It's been used to talk about computers playing chess, then machine learning, and now LLM-based systems.
Google's LLM here says:
Calling a Large Language Model (LLM) an "LLM" is a misnomer ...
Case closed /i
Advancement in capability does not mean the mechanism is the different. The LLM name denotes a very specific mechanism..
That is what all marketing wants you to think...
(Yes, pure math research is useless. Applied math is very useful, but he is doing pure math, which is very useless.)
https://arxiv.org/abs/math/9404236
He wrote it in 1994.
He writes about how he almost "destroyed" a subdiscipline in mathematics by becoming so good at it that he outclassed everyone. PhD students were advised to stay away from the whole field.
When he discovered this, he realized his error was that he was focusing on producing results, and not focusing on explaining his thought process. It's that thought process that is valuable in advancing the frontier - results alone won't do it. It didn't matter how many theorems he proved, if he was the only one who had the mental framework in mind on how to think about the whole field.
I'm sure we've come across abstruse books where every theorem has a rabbit being pulled out of a hat, whereas other readers find it intuitive. It's because the latter has developed a mental model for the discipline, and you haven't.
So he set about slowing down, and focusing on holding lots of seminars where he worked with other mathematicians to explain the thought process. Eventually others started publishing proofs of key theorems.
When people publish in a journal, they are not merely doing it to show the result. They are having a conversation with other mathematicians. If they cannot explain their own proof, they're not having a conversation.
This is why even decades after the Four Color Theorem was proved, plenty of mathematicians don't consider it "mathematics".
Useful thought, rather than hobbyist thought, seems destined to be the exclusive domain of silicon.
This is hilarious lmao
This is a big if, right? AI can still generate subtle or even silly mistakes that any normal human, let alone a mathematician, wouldn't make. Besides, math is more than just getting a conclusion but to understand and to generalize new ways of solving problems. After all, mathematicians are a curious bunch. To quote Hilbert's epitaph: We must know. We shall know.
Maybe we'll have some hobbyist dabblers, but any real progress will be done by machines that skip the human.
Most research mathematics is pure mathematics which is completely useless. No routing algorithms. It's only relevant because we (or at least mathematicians) are interested in it. So an AI producing incomprehensible proofs would be completely pointless. That's why Tao insists on the importance of human understanding.
What happens when it's the cats who get to decide what's published?
Not an ideal scenario, but that's exactly the situation here. Mathematicians decide what gets reviewed and published in a a top journal.
In the long run, this can and should make journals obsolete.
I don't think you can be coherently pro-AI without thinking that the human brain will be obsolete, unless you believe in some inherent magic that the brain is imbued with. The only other option is that you haven't thought through the long term consequences of the innovation.
That doesn't mean they don't provide any value of any kind to anyone.
To your first point. There a large number of cases that maps can be reduced to. Very few people have checked these reductions themselves. In 50 years there will be no human alive that will have checked the reductions by hand. Do we then discard the theorem? More importantly, do we trust the people that claim to have checked all the reductions? There are hundreds of cases. I trust a computer verification much more than I’d trust human verification. Humans will likely make mistakes due to the tedium. And some will claim understanding of all cases but be wrong in their understanding in some of the cases.
But the point is that pre-AI it was already the case that famous results were published that very few could understand or digest. I think it is reasonable to expect that we will soon be at a point that Lean says a theorem is correct but no human can or will ever understand the proof.
What if Lean verifies Mochizuki’s proof of the ABC conjecture. Do we disregard it becuase no other mathematician understands the proof?
A few different reasons why use an LLM when mathematics is done for its own sake:
Formally verifying my proofs catches any mistakes I make, but verifying is also hard work. LLMs shaves off a lot of time when formally verifying a proof.
I can still read through an LLM generated proof and understand it. This is a way for me to understand the result I am working on (usually in order to know what to prove next, results are not proven in a vacuum).
My experience thus far is that, while correct, an LLM generated proof is often unnecessarily complicated or inelegant. I take pleasure in elegant proofs and will spend time iterating on the first proof until I find it conveys the idea in the most elegant way. Having the initial LLM proof to start with is really useful, but is thus far rarely the final product.
AI doesn't have to implement Hilbert's vision and be able to prove everything. I just has to out-prove human mathematicians.
In many situations, people doing this, skillfully even, has had quite pernicious consequences.
I could prove anything by claiming I completed a trivial-to-explain exhaustive search. The only support or refutation would be someone doing their own search. It's a very weak foundation.
We already had the ABC conjecture crisis: A theorem with a human-written proof so complex that no one besides the author can understand it. Some people claim to have refuted it. Most mathematicians are unqualified to decide.
https://terrytao.wordpress.com/2026/08/18/palomar-a-registry...
Edit: I just saw Tao actually mentions the above essay in his paper.
Once AI starts under its own direction, human brains won't be competitive. It feels like we're a breakthrough or two away, and with trillions of funding, we'll get there. Every dollar we spend on Claude subscriptions gets us closer.
It is going to be a tiny minority of people who "win". The other 99.5% of humans will just be losers who, what, die in the streets? This argument reminds me of Roko's Basilisk. "The humanity-ending torture-loving Basilisk is coming whether you like it or not, so come over here and help me build it!"
The stochastic parrot of my reference is not a meme.
https://en.wikipedia.org/wiki/Stochastic_parrot
The term was introduced in a 2021 paper on AI ethics titled "On the Dangers of Stochastic Parrots: Can Language Models Be Too Big? " that was authored by Timnit Gebru, Emily M. Bender, Angelina McMillan-Major, and Margaret Mitchell.[a]
> The bots' output may be annoying to read but they're clearly onto something
Sure. Next-token prediction with huge source set and computation power. Nothing new there.
I would use a different adjective: exceptional.
There are not not times where lone geniuses produce amazing output. But most of humanity's progress over the last few thousand years (or at least certainly the last few hundred) resulting from a different type of work.
Referring to my list of examples as exceptional in the sense of being rare is rather unfair, given how numerous these examples are relative to the body of mathematical work we would consider incredible and especially relative to the desire of the average human to socialize. The fact that such a large % of that body of work occurred while the individual was in relative isolation is something we should pay attention to.
I don't follow - are you surprised that mathematicians have social rules on how they interact with others?
You're definitely welcome to set up a journal that takes whatever types of papers you deem acceptable. It's not like they're preventing the dissemination of information by taking this stance.
Personally, I wouldn't hire a SW engineer who only showcases output from LLMs, and can't explain the code it wrote.
Since even the engineers that know what's going on aren't actually reading all of the AI output any more (or, if they are, they're not keeping up with their peer's output), why would you care? I don't think humans should waste time trying to understand their code, it's too slow and costly, and the understanding will be blown away the next time the AI changes it anyways.
Software engineering is becoming pasting in vague-ish descriptions of what you want, and then manually testing that what the AI developed is close enough. It seems like math can go in the same direction too, with useful results that improve our technology getting put into a database for other AIs to consume. Removing humans from the loop can speed things up, especially as AI improves, especially when it reaches a self-improvement loop.
As I keep saying, software is no longer skilled labor. Who knows, math may go in the same direction.
In that setting, field experts working at the bleeding edge are so advanced that non-experts literally can't understand what they're saying at all. So there's a whole class of specialists, "synthesists", that specialize in gaining approximate understanding of the experts' work for the purpose of communicating it to outsiders—perhaps wrongly, according to the expert at least, but hopefully more productively vs the unmediated version.
https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o...
> In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.
The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
(N.B. from August 2026)
My point was rather more motivated by having seen so many weird ways for machines to fail/not work as expected that I wonder how to deal with that if the output were to be incomprehensible to humans.
(I don't know why you're so butthurt BTW - neigher of your ad-hominem comments actually outline your concern)
It's mostly memorization and recall and a single proof about primes he is well known for. It's akin to being well versed in Star Wars canon.
If Tao can be replaced by a model he isn't that smart just hyper-optimized in a narrow scope. As a scientist such evidence has to be a part of the assessment; it's not hard; find gaps in a syntax system and generate meaningful syntax to close the gaps. It's an idea printed in information theory books almost a century old.
He's well versed in existing content but has broken no interesting new ground. Where is his calculus or linear algebra. That to me is the real bar; definition of truly never before seen axioms and proof of them.
Lewis Hamilton is a great car driver but he didn't invent the internal combustion engine or racing; he's just a butt in a seat.
Butt hurt; because I don't easily accept awards handed out by innumerates who, not being mathematicians themselves, cannot possibly have an informed opinion on the quality of his work.
Many a mathematician and physicist out there have claimed there's no telling how much of this is verified; there are endless papers out there that constrain what we can actually know via scientific inquiry. Everyone in research just pretends they know it all because hey it's a living made not working in the mines.
But my bad for discussing and debating this all with experts over the years and not just accepting the populist take. If going with popular thing is the expectation Christianity is way more popular around the globe; lets just bin this science thing.
Good for Tao for achieving celebrity in a world of willfully ignorant people; convincing people too ignorant to challenge him to just give him awards sure means those awards are meritorious.
I simply don't carry water for and deify individuals when everything is clearly due to a mesh web of human labor across the globe.
No, not really. This is just the term that stuck around. The "large" is now up to five orders of magnitude larger and "language model" has gone far beyond any simple notion of modeling a singular natural language. And anything you'd cite about transformers, or tokens, or autoregression, etc., is more of a factoid about what works best and happens to be the most convenient in the here and now. I see all of this as an unbroken continuation of work that's been going on since the 1940s.
Instead of trying to play word games, why can't you just read Tao's article?
Does not matter. It is still an LLM.
And I am not the one who is playing word games. You and your idols are, for sake of marketing.
There is an LLM acting as a component in a larger system. But that larger system is not an LLM. Calling it an "AI" is indeed an act of marketing as there is no learning / adjustment as we would expect from an intelligence, but calling it an LLM seems to be inaccurate. So what is it?
Cool. So now you can accept that "LLMs" are an obvious example of AI.
>You and your idols are, for sake of marketing.
Let's be very clear here. Terence Tao is arguably the greatest mathematician alive. Yet, you are throwing lazy insults and accusations around because you don't like the term "AI". And that's my final comment for you, troll.
One tragic thing about all of this is that unlike almost every profession, mathematics actually has a kind of honesty. You honestly solve the problem or you don’t. The pecking order in mathematics at least used to have a grounding in actual abilities. People respect this guy because he’s actually legit.
(I’m not sure the extent to which you think this is marketing. I’m operating under the assumption that you agree with his Hypothesis 4.1. If you don’t, then I’d assume you haven’t seen the long list of prominent open math problems that these systems are providing answers to. And if this doesn’t sway you about Hypothesis 4.1 I’d just halt and ask why.)
And oh, what a stride it is: https://vibemathed.com/stats
Why does this tend to be the case, even when some of the smartest people in the world have historically predicted incorrectly that certain branches of math would forever be useless (e.g., number theory)? I can only offer my own theory on that, but my guess is that mathematics is simply a predictive framework based on pattern compression. A more powerful pattern compression framework accelerates every single field that relies on pattern recognition or prediction of the unknown based on patterns.
The output might make a cool screen saver as-is, but we probably need a way to evaluate it somehow.
Let me make up an example of where I could imagine this going. Something we essentially cannot do right now is predict coarse-grained phenomena from systems that involve millions or trillions or more of interacting components. Over hundreds/thousands of years of experiment and theory we've derived laws that essentially do this in a few special cases, but we have no systematic theoretical way of doing it in general, and frankly I think it's beyond human ability. Whatever deep patterns or structures exist for doing this in a general way I think are simply out of reach for us.
That's a misconception. Only a tiny percentage of mathematics has seen any applications whatsoever. There are vast libraries full of mathematics no one (in this discussion, anyway) has ever heard of that no one reads anymore and has never been applied to anything.
This idea of trying to "prove all the math" with AI makes as much sense to me as using chess engines to try to "solve chess."
And that's an issue why? It would seem to me that producing that also produced the mathematics that revolutionized the world repeatedly for centuries. I would go further and claim that, if you want the mathematics that revolutionizes the world, there's no way to get it without advancing mathematics as a field broadly. Those are not two separate activities, and thinking that they are is indeed a misconception.
> This idea of trying to "prove all the math" with AI makes as much sense to me as using chess engines to try to "solve chess."
You're right: "prove all the math" does not make sense on any level, and nobody serious would phrase any of this in that way. I certainly didn't.
Terence Tao
Sir Andrew Wiles
Grigori Perelman
Peter Scholze
Mikhail Gromov
Not sure what this has to do with what I said. A lot of things have been called "AI" in various times. None of them including the current crop of LLMs are not really AI. But people use AI term loosly and that is fine. But it is a problem when a some thought leader does it.
>troll.
Tell me you have run out of arguments without saying you have run out of arguments...
What does it say?
Again, this is literally the name of the field (and the tech). It's been around longer than you and probably your parents.
Dartmouth workshop (1956):
https://en.wikipedia.org/wiki/Dartmouth_workshop
Random dusty undergrad textbook from the early 70s:
https://m.media-amazon.com/images/I/816fxHVJkHL._SL1500_.jpg
>there is no learning...
If human-like continual learning is suddenly the standard, you can just as easily say that terms like machine learning and deep learning are an "act of marketing".
"every aspect of learning or any other feature of intelligence can in principle be so precisely described that a machine can be made to simulate it."
Clue: If you put a pig in a poke, is it still a pig?
The issue is SNR: signal to noise ratio. Generating exponentially more mathematics, particularly if the process is indiscriminate or optimized for something other than usefulness or mathematical relevance (such as optimizing for machine-provability), does not imply that we get exponentially more applications. We may end up halting the progress of applications altogether as the entire capacity of the world's mathematical apparatus is consumed by the interpretation and investigation of machine-generated proofs.
You can already visit arXiv and find vast numbers of not-yet-published mathematical papers. Most should never be published. None of this junk is benefitting humanity in the slightest.
Moreover, the disdain you have for low-value output in mathematics is not unique to you. Talented mathematicians don't like it either. Your mistake is assuming that AI will cause math to be dominated by low-value outputs. In fact, the opposite is likely the case: the marginal value of proofs will fall so low that the bar for meaningful research will become dramatically higher, not lower. I expect the goals of research mathematics to become extremely ambitious relative to the past, organized around substantial and enormous goals, not mass-generated slop as you're imagining.
Of course, yes, there will still be lots of slop, just like GitHub is full of AI coding slop, LinkedIn is full of slop, etc. But that's a generalized issue of the AI era, not unique to math.
I didn't say anything about low-value output. No one actually knows the value of any particular piece of mathematics within that deluge. Mathematicians don't have a magical ability to differentiate high-value mathematics from low-value merely by reading paper titles and abstracts.
The dirty secret in the mathematical world -- that has been going on for a long time already -- is that papers get attention based on the reputation of the authors, not on the rigour or validity of the proof. The big headline-grabbing papers are getting read by mathematicians because AI researchers have leveraged media exposure to bypass the reputation network, but media exposure doesn't scale.
When everyone is using LLMs to generate proofs, only reputable mathematicians will be able to get their work read. And herein lies the crux of the problem: an exponential takeoff in the volume of output from respected mathematicians will leave a critical shortage of readers.
it could end up being far easier to reasonably direct and evaluate the research direction and output of AI systems than human mathematicians
That's baseless speculation. All indications so far are that LLMs produce proofs far longer and far more complicated than humans are capable of, such that only machines can check the proofs for validity. Digesting them into a human-readable interpretation of the results is an open problem.
Being rich doesn't mean you can do whatever you want. But it means you can choose not to do what you don't want.
False. You very plainly did. You simply used the term “junk” instead.
> That's baseless speculation.
It might be speculation (as is much of what you’re writing), but it’s not baseless. Obviously, it’s quite easy to direct AI agents, a single one of which can pivot across all of mathematics, unlike all human mathematicians.
> All indications so far are that LLMs produce proofs far longer and far more complicated than humans are capable of, such that only machines can check the proofs for validity.
I’m unaware of any clear evidence of this. Hence, it appears to be baseless speculation.
> Digesting them into a human-readable interpretation of the results is an open problem.
I’m unaware of any clear evidence of this. Hence, it appears to be baseless speculation. Moreover, and more importantly, to my knowledge there hasn’t been any meaningful result in AI mathematics so far that has posed any kind of blocking issue on understanding it yet.
Suppose an oracle tells us the Riemann Hypothesis is correct. There are a vast number of results of the form:
If RH is correct then A.
It would be very useful to have an oracle tells us whether or not RH is correct.
In any case, I think it's better to read PP as somebody would find a practical, albeit incomprehensible, algorithm for solving NP complete problems.
Although I probably disagree with PP, because even a candidate algorithm that mysteriously works without proof would have practical value, so this case is not predicated on proving.
I think a better example of genuinely practical but rather uninteresting (YMMV) mathematical proofs are proofs of convergence of numerical methods, FEM for example. (I have been through it in school, it was a torture.)
Somebody, eventually, somewhere would understand it, or at least aspire to understand it. And even if he doesn’t, what have they learned in the process? About themselves, about their environment? About failure? I would bet a lot. How useful then, can we say that it is, not because we can understand it, but because we can try? That is useful. This is about the journey. Sometimes the journey is the point.
This is like if math was fascist, this is what would happen. When you start controlling the flow of knowledge like this, it will be bad news all around. And who is to say whether or not something can be understood?Aside from the math nazis.
If we are going to dictate what gets published like this, why bother publishing anything? This feels like a gatekeeping…that’s exactly what it is. Ya’ll getting nervous?
We only compute with two kinds of things:
- small data; or,
- extremely lower power and coefficient algorithms
We lack the power to, eg, use a quintic algorithm in anything but nearly trivial cases.
Furthermore, careful analysis of the latter would as likely as not yield further understanding and, actually /would/ help finding such algorithms.
Finally, it has been observed time and time again that often (again, nothing comes up and i don’t want to ask AI) the certainty that something is possible and has been done is motivation and inspiration enough for people to independently solve a problem. Sometimes it is even enough for someone new to simply not know that something is “hard” to solve.
It even “motivates” llms, it seems (eg https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...)
Of course this is all pure speculation concerning a hypothetical proof that most likely doesn’t exist, or indeed might be so complicated as to not be approachable even after hundreds of lifetimes of study.
Nevertheless your conclusion does not follow from the premise
You would need an algorithm that finds solutions, not just a proof they exist. So the value here would almost entirely come from how you proved p = np, since that proof will probably be the first step towards finding the polynomial solutions. But if humans don't understand it good luck finding any.
Is Amazon still delivering food to your cat?
Humans don't need to understand what AI generates. We still can get the rewards.
Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it, it initially seemed useless, then another AI system found a predictive model of electromagnetism using it.
Memorized proof patterns have value because they lead you to a final proof.
https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
IIRC he has expressed support in the past for attempts to formalize IUT in Lean, but we'll see where that really goes, because he's absolutely not clearheaded enough to lead such a project himself.
In history, we made much more use of hitting things with bows than abstractly comprehending arrow flight.
That said, without understanding, Math can't evolve. Comprehension of a proof is very important, but not what Math is fundamentally about.
Computer programs are Math. You can use them without understanding how they work.
When you have full AGI of course you no longer need humans to understand math.
> Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it
Developing multivariable calculus requires much more than just solving problems though, it requires defining an entirely new system and space. That is not the situation mathematicians face today, modern AI cannot do that.
When talking about mathematicians and AI don't use fictive examples, we can look at what AI can do today and extrapolate that they can do more of that tomorrow, that is what we have to work with.
In the case you posit where AGI exists there is no reason to even discuss what is left for humans to do, since AGI is defined as when humans are no longer needed for anything, the AGI can do every bit of thinking humans can.
Anyway, if we put the AGI framing aside, I think the main point you're making is that AI mathematics hasn't yet demonstrated the ability to theory-build in the way that the great human mathematicians have (Grothendieck, Scholze, etc.). And I'd agree with you on that. Where we disagree, I suppose, is I think that capability is coming -- I don't see anything that would prevent its development.
The idea of AI stepping from a graph theory/combinatorics innovation to some new and useful algorithm isn't crazy.
If I understand you correctly, you're just qualifying that that will only be the case when AGI exists. To be clear, I actually disagree with you here because I think it's very plausible to find a use case for human-incomprehensible math proofs before AGI exists. I'm just saying it sounds like you're agreeing with the parent comment that math is not purely about human comprehension.
Secondly, there is no truly objective truth to the area of a triangle. At bottom, this “truth” is simply “everyone is convinced, and for good reason”.
Without persuading other people of the “truths” that you discover, there is no real mathematics.
Why? If I sat around and studied math by myself and discovered something true yet not yet known but didn't share it, it's still true. Are you saying I didn't "do math" because I didn't share the result? Math exists on another plane and it has 'truths' that we haven't discovered, yet are still 'true', no?
Math has been almost purely arbitrary since ~ late 19th/early 20th century. There are uncountably many correct mathematical theorems. Almost all of them can't even be written in symbols. Even if you have a tape with infinite length (which is already longer than the whole physical universe!) filled with theorems, they are still only 0% of all correct theorems. That's how arbitrary math is.
> The area of a triangle
Yes, even this is arbitrary. The rigorous definition of triangle is arbitrary. People just subconsciously choose something that vaguely approximates their physical intuition.
What are you talking about? A theorem is a statement that has been proved from some axioms. A statement itself is a finite sequence of symbols satisfying some syntactical rules. The set of symbols for set theory, arithmetic, etc is finite, so the set of statements, and a fortiori the set of theorems, is at most countable. Where do you get the uncountability?
I suspect you are confusing theorems and theories. Assuming the set theory ZF (for instance) is consistent, then a consequence of Gödel's incompleteness theorem is that there are indeed uncountably many inequivalent extensions of ZF that are complete and consistent. Also, not a single one of these extensions can be described in symbols in the sense that there does not exist a computer program that enumerates a possible set of axioms for the extension.
As for your general point about arbitrariness, the late 19th century was a period when mathematicians started being concerned with the rigorous formalization of mathematics. Sure, there are some arbitrariness in the particular choice of formalization in the same way that the particular form of a programming language like C is arbitrary. However, the Gödel stuff has nothing to do with that arbitrariness, it is about the limit of formalization itself. The programming analogue is the undecidability of the halting problem. Saying that mathematics are arbitrary sounds to me a bit like saying that an algorithm like Quicksort is arbitrary because you saw an implementation in C and the particular form of the C language is arbitrary. Obviously, if you don't like the C language, you can implement Quicksort in another language. The same is true for mathematics. If some day, somebody finds a contradiction in ZF, or simply a new formalization that people find more convenient, then most mathematics will simply get translated and very little will change.
Whatever philosophy you prefer, math is about establishing objectively valid logical results, completely independent of the human process used to arrive at them.
it starts as a tool for humans, then evolves into a set of interesting properties of those tools, then grows into an art form, a set of "games" where cooperation is half of the point. the other half is discovering beauty in this weird parallel world of our reasoning and imagination. once tools become autonomous and start making up their own games we can't even play then mathematics loses it's meaning as a discipline. the only retort you can come up with is that "it's going to be useful". how would you know? because your autonomous tool that's too smart for you told you so? they could be as useful as morning orange juice to Claude Shannon was in terms of inventing information theory. I.e. you drinking it won't make you any closer to inventing anything of the sort anytime in your lifetime.
do triangles exist IRL? is the world discrete or continuous? can you prove it? If you have an answer to all of those I know you're wrong.
also in your computer program example just shows you don't understand it at all. those programs ARE NOT understood by you, but someone else who built them did. someone who bothered to read and architect it did. The whole Google codebase might be incomprehensible in its totality if you go bottom up but it is comprehensible by construction by us. Same with math. You don't understand all the bits of it, but someone built every brick and so you know it is "true". once the bricks become black boxes you're screwed.
You seem to be vaguely waving in the general direction of a point, without making any concrete claims or bothering to engage with the GP’s argument.
The tastes and interests of humans are absolutely not arbitrary. They are dictated by fate, the sun and the moon gods. Or maybe by the unitary evolution of the universe’s quantum state. Or by the probability distribution of finding ourselves in a particular branch of the universe.
What bearing does this have on whether math is a collaborative endeavor?
And what is unique to math, that your argument wouldn’t apply equally to physics, sociology or financial markets? All, “truth seeking” disciplines.
Nonetheless, the person writes, “ Math has been almost purely arbitrary”.
This is simply a misusage of the word arbitrary, which is a word with a specific meaning you can look up if you are unaware, since mathematics is (obviously) not arbitrary in the sense this person wants to convey, in part for the reasons I state. Humans are not choosing arbitrary logical statements to prove true or false.
Mathematicians even argue which axioms we should have, it isn't objective in the slightest, mathematics is therefore very closely linked to our feelings and intuition. Remove that and you just have formal logic, a very different field.
From my perspective, I feel you restated what I said with the opposite conclusion. You say that axioms "defines" mathematics. If I were Claude, I'd say that the word "define" is doing a lot of work, is load bearing or something like that.
"Define" is where we turn these axioms into consequences - what I call "truth". As opposed to all the other stuff people could say that don't follow from these axioms. These are nonsense and, most certainly, un-mathematical.
> Oh it would change a lot. It would be an enormous psychological boost for everyone to find a practical algorithm.
OK, I tell you that P=NP, and that I am a magic oracle. So, you have you psychological boost for finding a practical algorithm for free. :-)
a) I am already convinced that P=NP
b) You have to convince many other people as well (that you're a magic oracle), because for the effect to work, lot of people would have to work on the problem (or at least spend tokens)
Nevertheless, a plausible magic oracle (such as Lean-verified proof, even if non-constructive and incomprehensible for humans) would convince many to take a 2nd look.
It would not not necessarily be practical, even if it ran in polynomial time. It may have cost O(n^c), with a totally out of order exponent like c=A(5,5) or whatever.
In reality, it wouldn't depend on the truth value of the statement, but on the AI understanding the proof. If it understands it then it might be able to use it to find reductions.
So the point remains, knowing that P=NP isn't what's important, it's the proof that matters.
The area of a triangle doesn't have 1 unique formula, it has many, depending on the system you use. A triangle in plane geometry has a different area than a triangle in spherical geometry, and different again in hyperbolic geometry.
When you get to studying the geometry of manifolds, you realize the area of a triangle can be any damn thing you want, depending on how you construct the manifold you embed it in.
A proof can just be "assuming these axioms.....the area of a triangle is X"
We all believe it. It's a magic oracle. Now what?
But one can already study the consequences of P=NP right now. You don't need to know that it's provably true in order to do that.
Knowing an actual proof would be useful, but an oracle revealing merely that it's true (or even provable) without telling you the proof does not let you do anything you couldn't do before.
For what? Which product becomes better if it is correct?
I have published mathematics so I do value knowledge, but for most of mathematics the value of the knowledge isn't the thing you try to prove it is all the things you learn as you try to prove it. p = np is one such thing.
So the whole interesting bit about it is the proof, not the fact.
For what? Which product becomes better if it is correct?
This sentiment is anti-thetical to the whole point of pure math and theoretical science. No product became better when Euler proved the fundamental theorem of algebra.
Tying the worthiness of theoretical knowledge to the whether or not it improves a product is asinine in my opinion.
[0] and am only adding that "generally" because I can think of examples where I'd disagree, e.g. a kid that wants to count all stars in the night sky before it has dinner would just starve and then not be able to count stars, either.
A lot of people spent a lot of time and effort to prove or disprove the Jacobian Conjecture. AI solved it easily. It is increasingly becoming the case that humans are not as good at mathematics as computers. You are free to ignore computer generated proofs but I don’t think this position will win out in the long run.
No, people constantly prove statements of the form "if P=NP, then strange implication X". They do not consider it wasted effort at all, because of the contrapositive: if X is indeed very strange, they might be able to prove that it is false, and then they've settled P!=NP.
At some point an AI will prove a result that is so long and complicated that no human will understand it. This should not preclude people from using that result. In general, whenever the body of knowledge is increased it is a good thing. Even if it isn’t increased by humans.
