Rendered at 01:34:27 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
sonicrocketman 8 hours ago [-]
Tao's Rule of Thumb (which applies very well to software):
> 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.
kriro 6 hours ago [-]
The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really hard to explain to humans, even by GMs. They can sort of explain that something is a good line but not why. Engines crush GMs and are considered ground truth even if noone really understands what is happening. Would it be a nightmare if math was the same, not sure. Especially for counterexamples LLM solutions seem fine. They stop humans from wasting time on pointless things. For proofs it gets more hairy but I think if it is formally verified a proof is a proof. Attribution is a problem (should the person who wrangled the answer out of an LLM get the credit, I guess so).
I think these are non-trivial epistemology and science theory problems.
zahlman 3 hours ago [-]
I don't think this is a valid counterpoint at all. Math is cooperative, and comprehension is the point: the proof has value exactly because (and only to that extent) it empowers humans to understand an abstract truth. Chess is competitive: the memorized line has value because it makes you incrementally more likely to defeat your opponent.
thechao 2 hours ago [-]
I hope I'm remembering this right: a mathematician claims to have a proof for the ABC conjecture, but can't conceive any other mathematician it's right — it's "too weird", so the proof is rejected?
sanxiyn 56 minutes ago [-]
The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything.
Not quite?
It is more that
1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person
2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
glimshe 1 hours ago [-]
Math isn't "cooperative". Math is about truths. The length of circumference. The area of a triangle. The formulas for these are true in an objective sense irrespective of whether you understand them.
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.
gsinclair 56 minutes ago [-]
First of all, mathematics is about so much more than the area of a triangle etc. that any analogy based on such simple things is overwhelmingly likely to be too simple to be of value.
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.
d4v3 39 minutes ago [-]
> 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?
raincole 44 minutes ago [-]
Math is not about truths, at least not by the meaning of "truth" as a word in daily use.
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 intuitive.
rain_iwakura 37 minutes ago [-]
this is primitive understanding of math. what does "truth" mean here? usually arguing over definitions is something i hate, but that's the whole point of mathematics.
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.
nilkn 2 hours ago [-]
Math that humans don't understand but nonetheless allows AI systems to develop breakthroughs in various fields of science, technology, physics, engineering, medicine, etc., would have great value to humanity even if it doesn't help humans understand abstract truth at all.
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.
GPerson 5 hours ago [-]
I don’t think it’s pointless to spend time trying to prove a conjecture which is ultimately false if along the way you figure out a bunch of different true variations on the conjecture, which is how mathematics actually works. This is something I’m a bit worried about with LLMs since it gets you to the end too fast.
ianm218 3 hours ago [-]
LLMs seem to have worse intuition than experts and compensate by being able to cover a much wider surface area of ideas, so we might just need to extract the intermediate progress along the way.
jhrmnn 5 hours ago [-]
I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?
metahuman_crumb 4 hours ago [-]
I suggest "Catching crumbs from the table" by Ted Chiang. Very short piece published in Nature (2000) and well worth a read. Depicts a scenario where modified humans produce science beyond ordinary scientists' comprehension.
cfiggers 4 hours ago [-]
This is a theme in Blindsight by Peter Watts as well.
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.
cfiggers 2 hours ago [-]
What's amusing to me in this context is, summarizing emails and such has for a while been a supposed use case for AI—the LLM serving as the "synthesist" to explain long texts accessibly. But with this math question, a human "synthesist" would be needed to approximately understand the math discovered and programmatically verified by the LLM. So the roles reverse.
JadeNB 3 hours ago [-]
Presumably there's not much logical obstruction to all human-understandable math eventually being formalized, although the willingness and ability to commit the requisite enormous amount of time will probably be insurmountable. But definitely that hasn't happened already!
Jblx2 4 hours ago [-]
Mochizuki enters the chat
OhNoNotAgain_99 4 hours ago [-]
[dead]
fukaiall 2 hours ago [-]
Mate you managed to provoke with this comment. But you know what you’re saying right?
RandomLensman 4 hours ago [-]
If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?
Jblx2 3 hours ago [-]
Yes, you still need to be careful, especially if you have reason to think that the proof was from a malicious actor.
The whole point of Lean is that you don't need to understand the entire proof to be sure that it's correct. You only need to understand the definition of the theorem being proven, and you need to trust that the relatively small core of Lean is correct.
raincole 26 minutes ago [-]
I don't think Lean is as rigorous as you implied here.
> 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.
RandomLensman 3 hours ago [-]
Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
rowanG077 2 hours ago [-]
Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
gowld 2 hours ago [-]
Why should you trust that the relatively small core of Lean is correct?
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.
patcon 3 hours ago [-]
Sincere question, as a non-expert trying to situate your comment: are you a mathematician with experience in proofs?
RandomLensman 3 hours ago [-]
My time proving things is long in the past and any systems way back when I was studying (some math among other things) certainly were different and usually quite narrow.
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.
gowld 3 hours ago [-]
Math humans can use but not understand is called engineering.
-- paraphrase of Bill Hammack, https://engineerguy.com
I believe this rule of thumb will come to fail. The combination of superhuman mathematical reasoning and synthesis in upcoming AI models plus the rapid build-out of scalable formal verification infrastructure means this exponential in math is going to take off quite explosively, and we've barely seen anything yet. Mathematics is going to decisively move beyond human ability fairly soon (within our lifetimes, if not much more abruptly). It seems abundantly clear to me that much of the work will only be immediately accessible to AI, and rather than trying to explain all of it back to humans we will rather focus on explaining the portions that humans would benefit disproportionately from understanding.
skybrian 5 hours ago [-]
Maybe that will be true when it's math with practical applications, but most theoretical math isn't like that. If it's not practical and it's not for mathematians to understand, what good is it?
nilkn 2 hours ago [-]
We have thousands of years of precedent that suggests that breakthroughs in mathematics tend to accumulate into broader technology breakthroughs in other domains.
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.
skybrian 1 hours ago [-]
It sounds like the idea is to turn on a math generator and keep running it until it generates something interesting. And it might be fun to try it. But if it’s too much output to read and we don’t understand the output either, how does anyone recognize when it’s done something that’s practically interesting?
The output might make a cool screen saver as-is, but we probably need a way to evaluate it somehow.
nilkn 54 minutes ago [-]
Yes, of course we'd need a way to evaluate it. I don't right now have a fully conceived answer to what that will look like. But I'm confident at least in saying we would not evaluate it, like Tao is suggesting, by only accepting something once a human can easily teach it unassisted to another human. That sets the bar dramatically too low and would quickly become an extraordinary impediment to progress. You'd have to think of yourself less like a researcher and more like the director of the world's largest research institute. It's highly unlikely you'll understand or even care about every single paper every one of your researchers is producing, but you'll care about the overall research direction and whether the intermediate results are accumulating into outcomes you consider meaningful. How to do this where the institute is based on superhuman AI mathematicians is an unsolved problem, but I see no reason to imagine it's unsolvable.
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.
cma 3 hours ago [-]
You could have one really hard to understand proof of a theorem and then a lot of interesting human-understandable stuff that relies on that theorem. We already have lots of proofs with oracles, where you can work out consequences of what kind of structures and solutions could exist if you had some magic thing to solve a hard part, so it just seems like a variation on that. Many people learn calculus or even the real numbers without understanding the complete formalization from set theory.
esafak 4 hours ago [-]
One day it might be for the AI's pleasure, the same way it has heretofore been for ours. Or if you prefer, as a byproduct of its programming to acquire knowledge.
fultonn 4 hours ago [-]
People say similar things about automation of software engineering. Different, but similar.
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.
[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.
3 hours ago [-]
raincole 48 minutes ago [-]
The problem is that there will be far more formally verified proofs than that human mathematicians around the world can read, much less explain. What then? Would the role of mathematicians just become explainers of AI generated proofs?
czgov 8 hours ago [-]
I wonder what his views on the 4 color problem are. One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases. It doesn’t take an expert to state this.
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.
akk0 6 hours ago [-]
For an exhaustive search, if you can explain to me:
- how to exhaustively list the cases that need to be checked, and why that method is exhaustive
- how to check each case, and why that works
and then conclude with "we've had a computer do this exhaustive search, and the result came up as X", for me that satisfies completely understanding the proof.
gowld 2 hours ago [-]
But the "computer" is magic, to you.
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.
odyssey7 34 minutes ago [-]
If you prove that the theorem prover’s true and false determinations are correct—in the cases in which it can make them—then Bob’s your uncle.
ChadNauseam 7 hours ago [-]
> One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases. It doesn’t take an expert to state this.
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
czgov 7 hours ago [-]
That will certainly happen. Humans will extend AI generated results. But what will also happen is that AI can “think” much longer than a human can and can have a vastly greater base “knowledge” than humans can have and so there will be a bewildering amount of new results. Humans may not be able to keep up.
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.
aleph_minus_one 6 hours ago [-]
> I wonder what his views on the 4 color problem are. One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases.
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
intuitionist 6 hours ago [-]
Nowadays the proof of resolution of singularities in characteristic zero is considered something you can teach in an intro algebraic geometry course, though. The concepts have been absorbed and are now much better understood. 4CT is very different because so much of it is exhaustive case analysis; you can understand the high-level ideas of the proof as a bright undergraduate, but you still can’t check the cases by hand
czgov 4 hours ago [-]
Abhyankar and others spent years trying to find an easier proof. I’m not an algebraic geometer and I don’t know the state of things now. I was under the impression that on the level of Ideals, Varieties, and Algorithms one can introduce the concept and do some calculations but not present a proof of the theorem.
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?
8 hours ago [-]
odyssey7 38 minutes ago [-]
This is a statement about what Tao values in the proofs that he consumes, as a world-class, human mathematician.
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.
lacker 5 hours ago [-]
I don't think the mathematicians are going to be able to make that work, because journals are already struggling to keep up with their review load, and AI seems like it will make that harder. So a solution that involves "journals will do a lot more effort to review each paper" doesn't seem practical.
It would work better as a bar for hiring, rather than as a bar for publishing.
Jblx2 4 hours ago [-]
It will be interesting to see the evolution of journals in the next ten years for sure. Have they outlived their usefulness? Maybe everyone will just upload papers to arXiv, along with a copy of the formal proof.
rowanG077 2 hours ago [-]
Just package the proof as a library and put it in some source code repository like github.
mlmonkey 2 hours ago [-]
What if the result is a counter-example? A fact that disproves the conjecture? Is that not publication-worthy?
pfdietz 6 hours ago [-]
The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen. People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up.
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.
BeetleB 5 hours ago [-]
> People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up.
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.
cubefox 5 hours ago [-]
> The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen.
He says it shouldn't be able to published if they can't explain it. Publishing it is the reward.
pfdietz 4 hours ago [-]
The thing is, the cost of creating these results, and the expertise needed, is being greatly reduced. So it's possible for people who wouldn't actually care about the results to spoil them by just putting out a formalized proof (for example, to Tao's Palomar site). These people wouldn't care about the prestige; they aren't on a career track where that would matter.
rowanG077 2 hours ago [-]
I just don't see that to be true. If tommorow someone pulls a proof that n = np out of their ass but is not able to explain it, it will still have immense value.
tossandthrow 5 hours ago [-]
I think any idea that is contingent on a human being in the loop, solely to the property of being a human is most practically doomed to fail, but is inherently anti scientific.
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
_doctor_love 4 hours ago [-]
I saw an analogous argument posted on LinkedIn the other day from one of the opencode guys: the job of a programmer is still to be able to answer questions - from memory - about how the system works and why.
mohamedkoubaa 6 hours ago [-]
Ive wondered whether a possible outcome of LLM slop is a retvrn to oral wisdom traditions. Ironically that's the most anthropological form of understanding and pedagogy.
highfrequency 8 hours ago [-]
Terence Tao's quote about AI's math proofs is relatable outside of pure math: "the writing very often dwells at length on trivialities while passing briefly through — or even actively obscuring — the most interesting and novel portions of the argument."
TMWNN 5 hours ago [-]
>Terence Tao's quote about AI's math proofs is relatable outside of pure math: "the writing very often dwells at length on trivialities while passing briefly through — or even actively obscuring — the most interesting and novel portions of the argument."
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.
jltsiren 3 hours ago [-]
I noticed another thing a long time ago.
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.
paulpauper 7 hours ago [-]
Similar to Ai writing. Lots of bloat.
piker 6 hours ago [-]
Coding, too.
itissid 3 hours ago [-]
What is being made is "what are our core values?" argument. One does not need to be a mathematician to know how poorly this worked for large communities when incentives are misaligned...
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?"
I don't know why anyone should care about understanding the results if the AI is better at math than us. It'd be like demanding that human mathematicians are banned from publishing until their cats understand the theorems.
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.
BeetleB 5 hours ago [-]
The essay On Proof and Progress in Mathematics by a Field's medalist is worth reading:
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".
a2ff6eeb0 5 hours ago [-]
I don't understand why people are so fixated on the minds doing the mathematics being made out of meat. It seems obvious that soon, minds made of meat aren't going to be able to keep up.
Useful thought, rather than hobbyist thought, seems destined to be the exclusive domain of silicon.
BeetleB 5 hours ago [-]
> I don't understand why people are so fixated on the minds doing the mathematics being made out of meat.
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.
a2ff6eeb0 4 hours ago [-]
Would you hire a SW engineer that only showcases output from compilers, and can't explain the assembly that 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.
FuckButtons 6 hours ago [-]
If you are free from physical and mental labor, you are in fact, not supplying labor, and are therefore surplus to requirements.
auggierose 4 hours ago [-]
Whose requirements?
esafak 4 hours ago [-]
The employer's, whose salary affords your subsistence.
hintymad 6 hours ago [-]
> I don't know why anyone should care about understanding the results if the AI is better at math than us
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.
bayesnet 6 hours ago [-]
It’s a bit of an ominous quote given that Hilbert’s program was dismantled shortly thereafter by Gödel…
pfdietz 6 hours ago [-]
I'm reminded of the joke about the two friends who come across a bear in the woods. When one puts on running shoes, his friend chides him that he can't outrun the bear. He responds, "I don't need to outrun the bear, I just need to outrun you."
AI doesn't have to implement Hilbert's vision and be able to prove everything. I just has to out-prove human mathematicians.
a2ff6eeb0 6 hours ago [-]
Well, that's why we have automated proof checking. And again, I don't think humans will be able to solve problems at a commercial scale in the future.
Maybe we'll have some hobbyist dabblers, but any real progress will be done by machines that skip the human.
fooker 3 hours ago [-]
Your analogy is great.
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.
TSiege 6 hours ago [-]
I’m not anti AI but thinking the human brain is obsolete and using it will become a hobby is a dystopian view of the future where no one has any agency anymore. By your logic since our brains provide no value why not just shoot ourselves in the head while we’re at?
a2ff6eeb0 6 hours ago [-]
What's wrong with sitting on the beach with a bottle of wine for eternity, with no need to do anything, knowing that all your needs and desires will be automatically taken care of?
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.
Jblx2 3 hours ago [-]
Are dolphins obsolete?
Calazon 2 hours ago [-]
I think they meant obsolete relative to economic, scientific, and engineering objectives.
That doesn't mean they don't provide any value of any kind to anyone.
applecoffeecake 4 hours ago [-]
If a result has a real-world application, then it can easily be published in an engineering or applied scientific journal in which it is already the norm to present methods that work empirically with little to no understanding of how.
cubefox 5 hours ago [-]
> If Amazon uses AI math to come up with better routin
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.
a2ff6eeb0 3 hours ago [-]
If it's just a hobby, why would you use an LLM at all?
mohamedkoubaa 6 hours ago [-]
What if the better routing leads to an outage that the AI can't explain or fix and all the humans who might have understood it were laid off or otherwise unavailable?
caglaroktay 6 hours ago [-]
AI also can replace a lot of expert attention too. Why not? What is useful or what is not useful is based on the expert's narrow opinion. An AI system can do much more and deep value comparison. It looks like if our current technological advancement continues, in the space of what is possible (or even impossible), AI can find the optimal solutions better than any human or human organizations. But I think there is only one think will remain for humans to go for these solutions: what we value. that will be the last resort I believe and hopefully ai systems won't start manipulate us too as we are very fragile on manipulation.
mmoll 6 hours ago [-]
But how would „what we value“ still be relevant?
sonicrocketman 9 hours ago [-]
Anyone else print their white papers before reading? (At least the short ones)
ivansavz 7 hours ago [-]
Absolutely. I feel I gain at least 10 IQ points when reading something on paper.
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...
magneticnorth 9 hours ago [-]
When I was in academia and had easy access to a good printer, I always did. I miss it now that it's easier to just read on my screen.
glimshe 7 hours ago [-]
Terence Tao sees a role for AI in science. I'm no genius but he basically described what I've thought all along... We don't need to be "all in" or "all out".
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.
GPerson 7 hours ago [-]
I think it’s more that he seeks to preserve and promote human understanding of mathematics, and sees that grappling with this new technology is necessary. One reason is that for human mathematical practices and institutions to retain legitimacy, they need to justify their value. As Tao explains, one obvious answer to that is made less obvious now with AI.
a2ff6eeb0 6 hours ago [-]
I think it's impossible to be half in. AI will eventually be better at things than people, and people will simply be rocks in the gears of progress.
The only thing to do is to be all in, or get run over.
evenhash 2 hours ago [-]
If what you’re saying is true, what’s the use (or even meaning) of being “all in”? You’re a rock either way.
a2ff6eeb0 31 minutes ago [-]
It's not there yet, and it's unlikely we're going to be building an equitable future. Unless things change, not everyone is going to benefit from AI. What are you doing today to end up on the team that wins?
rramach 8 hours ago [-]
Terence argues that explanation of results ("understanding") will be the new bottleneck in math research but I am not sure this is the real bottleneck for progress.
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).
tocs3 7 hours ago [-]
In some sense "understanding" (understanding if it is true, if it is important, how to use it) is about the only bottleneck in math. Any theorem that you can write down or imagine is already true, false, not provable already. In some ways we can already start iterating through all the theorems. We will never get to the end (or really get very far down the line) and most all of them be trivial (I think the Busy Beaver[1] project is a fascinating example, ymmv).
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.
Chasing these 'trivialities' is a good thing, imo.
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:
How is either of those situations more or less like a hobby than the other?
plastic-enjoyer 8 hours ago [-]
Somehow, I feel that progress, in your understanding of what progress is, loses all meaning.
paulpauper 7 hours ago [-]
It will be the same as before: some effort will go into checking proofs and the other into creating them. AI speeds up both.
cubefox 5 hours ago [-]
You clearly didn't read the paper.
ghm2199 4 hours ago [-]
Goal 6.4 reminds me always of the numerous times AI generated n PR's for a feature and I revolted and threw my laptop because it was incomprehensible or unworkable when viewed as a process/workflow.
tocs3 9 hours ago [-]
Maybe the Hitchhikers Guide to the Galaxy series was predictive in pointing out the problems of ill defined questions (The Answer to the Ultimate Question of Life, the Universe, and Everything).
paulpauper 8 hours ago [-]
Not using AI puts one at a huge disadvantage in a career setting. Ai can find deep references better than humans now, let alone actually doing the math. The challenge is knowing which problems to tackle given the cost limitations. If you have $10k to spend on tokens, you have to choose problems that can conceivably be solved within this budget.
nadermx 8 hours ago [-]
[flagged]
qsera 8 hours ago [-]
If the title have said in the age of "LLMs", I might have given it a try.
GPerson 7 hours ago [-]
You should give it a try. Tao is a wonderful person and is trying to help humanity.
qsera 2 hours ago [-]
> is trying to help humanity.
That is what all marketing wants you to think...
frozenseven 6 hours ago [-]
Out-of-hand dismissal of Terence Tao is certainly a take.
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.
qsera 2 hours ago [-]
>This is obviously no longer the case today.
Advancement in capability does not mean the mechanism is the different. The LLM name denotes a very specific mechanism..
frozenseven 37 minutes ago [-]
>The LLM name denotes a very specific mechanism..
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?
eloisant 4 hours ago [-]
"artificial intelligence" is a vague and moving target. I'm not sure I would call that "a field".
It's been used to talk about computers playing chess, then machine learning, and now LLM-based systems.
frozenseven 3 hours ago [-]
Of course it's been "used" to talk about those things, because all of those things are examples of AI. Always have been.
qsera 2 hours ago [-]
Then it has always been the age of "AI"...So the article title is inaccurate!
frozenseven 36 minutes ago [-]
We can meaningfully talk about (1) the existence of a field and (2) the said field hitting its stride. The title of Tao's article denotes the latter.
> 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.
https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
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.
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 intuitive.
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.
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.
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://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
(N.B. from August 2026)
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.
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.
https://www.youtube.com/@engineerguyvideo
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.
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.
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.
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
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.
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
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?
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.
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.
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.
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?"
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.
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.
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.
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.
AI doesn't have to implement Hilbert's vision and be able to prove everything. I just has to out-prove human mathematicians.
Maybe we'll have some hobbyist dabblers, but any real progress will be done by machines that skip the human.
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.
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.
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.
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.
[1]: https://bbchallenge.org/8226493
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:
https://wiki.bbchallenge.org/wiki/Main_Page
That is what all marketing wants you to think...
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.
Advancement in capability does not mean the mechanism is the different. The LLM name denotes a very specific mechanism..
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?
It's been used to talk about computers playing chess, then machine learning, and now LLM-based systems.
And oh, what a stride it is: https://vibemathed.com/stats