upvote
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.

reply
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.
reply
Math is also useful. If someone showed that p = np tomorrow in a formally verified proof I don't care if no one can understand it.
reply
If a magic oracle tells you p=np, that's useless. How would that change anything?
reply
I would hope the magic oracle would continue to tell me ways in which I can use this knowledge practically.
reply
If it’s an oracle and we know it’s an oracle then it’s not useless. Humans make mistake and there are examples of published results that were widely believed to be correct by experts that later proved to be wrong. Why do you think human verified proofs are better than machine verified proofs?

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.

reply
I asked how would it change anything. What's the next step if an oracle were to tell you p=np that changes anything about the world?

We all believe it. It's a magic oracle. Now what?

reply
If it is known that A is provably true then one can study the consequences of A being true. It changes things becuase the body of knowledge has expanded.
reply
> If it is known that A is provably true then one can study the consequences of A being true

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.

reply
In this case won't this oracle also tell you what is the consequences as soon as it tells you RH is true and also much more? At this point what is the point of you knowing what is true and what is not?
reply
> It would be very useful to have an oracle tells us whether or not RH is correct.

For what? Which product becomes better if it is correct?

reply
You have an unfortunate view of the value of knowledge. The frontiers of science would be static if everyone believed as you do.
reply
Someone claimed it would be "useful", without saying what for. Hence the questions "what for?". To try to shame people for that question in the name of science of all things is wild.
reply
The whole point why anyone cares about these proofs is that the things we learn as we make the proof might add value, proving p = np itself isn't interesting, that knowledge has no application and therefore no value in itself.

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.

reply
You are wrong as far as most mathematicians believe. The fact is important. The proof of the fundamental theorem of algebra is interesting and important but the theorem itself is also important.

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.

reply
deleted
reply
I thought the point of publishing was a matter of dissemination, to make available for people to then try to understand it? This is like saying, I don’t like music, so I’m going to tear down the venue. Then, all music genres suffer as a result, and all of society does, too. This idea is no good.

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?

reply
Oh it would change a lot. It would be an enormous psychological boost for everyone to find a practical algorithm.

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.)

reply
> a practical, albeit incomprehensible, algorithm for solving NP complete problems.

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.

reply
I know, the goal was to strongman the argument.
reply
deleted
reply
A proof by contradiction that p = np is of no use to anyone, given that it wouldn't help you find any polynomial time algorithms for np-hard problems.
reply
I don't think a proof that P = or ≠ NP would give you any polynomial-time algos for arbitrary problems either.
reply
I don’t recall anything specific off the top of my head but I am confident that such a proof would have immediate actionable implications.

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

reply
Abstract polynomial algorithms are of no use either, eg, translation may require galactic constants or high powers that are still intractable.

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.

reply
A proof that they are the same is of no use either, since it too wouldn't help you find algorithms that are faster.

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.

reply
How would the mere knowledge that it holds, without any understanding why, be useful?
reply
Can you explain to your cat how Amazon uses graph theory to deliver their packages of cat food?

Is Amazon still delivering food to your cat?

Humans don't need to understand what AI generates. We still can get the rewards.

reply
p = np doesn't produce any value though, the stuff you learn solving it might but the fact that they are the same wouldn't be valuable at all.
reply
sure, agreed, but once you have a proof, you can probably get AI to reduce other problems to that problem in P.
reply
Well then, just tell the AI that the statement is true and it will find reductions!

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.

reply
Why wouldn't you be able to do that without a proof? I don't see the value of the proof here, just ask the AI to solve the problem you want and the proof isn't needed.
reply
Why would it not be able to find reductions now, but be able to find them just by being told that P=NP is definitely true?
reply
From my understanding, the two are equivalent; if you can reduce an NP problem to a P problem, you've proven P=NP. The rest is application.
reply
Yes but it's also possible that there are other proofs. The point remains, the content of the proof is what matters, not that the statement is proven.
reply
[dead]
reply
[dead]
reply
The goals of Chess and Math may be different, but they follow the same principle of exploration large search space according to fixed rules. In case of Chess these are chess rules, in case of Math these rules of mathematical logic.

Memorized proof patterns have value because they lead you to a final proof.

reply
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.

reply
But at that point you have full AGI and its not just today's models. Today's models still need humans to understand things since it builds upon human knowledge.

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.

reply
It's reasonable to say that current or near future AI can find novel mathematical results and develop applications from those.

The idea of AI stepping from a graph theory/combinatorics innovation to some new and useful algorithm isn't crazy.

reply
deleted
reply
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?
reply
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.

https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...

reply
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.)
reply
Some of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…
reply
By this point, he is very much nutso enough that a Lean certified counterexample to his theories would not dissuade him. His response would be either that the formalization is incorrect (with no coherent insights on how to fix it), or worse, Lean itself is a tool of Western imperialism and incapable of properly explicating his ideas. He has, in the past, ranted against such things as monotheism and English grammar as being the reason for his theories' lack of popularity.

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.

reply
Project LANA ran into the same roadblock as Scholze and Stix, when they attempted to formalize the proof in Lean.
reply
[dead]
reply
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.

reply
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.

reply
> 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?

reply
No, they're saying that what is true in mathematics is contingent, not absolute. It all depends on which set of axioms use, what assumptions you make.

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.

reply
Sure, but just that some random statement is true isn't interesting. It's interesting if it helps understand some abstract structure better.
reply
It could also be interesting by having a practical use.
reply
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 intuition.

reply
The tastes and interests, and cultural pretext, of human beings are not arbitrary just because they’re not easily described.
reply
Yes and therefore?

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.

reply
This hasn't been a remotely reasonable characterization of math since at least Hilbert's time.
reply
I think Hardy would be very much on the same page with me, as well as Godel and many others. Mathematical truths exist independently from our feelings and processes to discover them. People do and should argue about which truths are interesting to pursue and refine, but all of them are out there to be discovered... or not.

Whatever philosophy you prefer, math is about establishing objectively valid logical results, completely independent of the human process used to arrive at them.

reply
Axioms don't exist independently from our feelings and processes, we pick axioms we feel are good, and axioms defines mathematics.

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.

reply
Is formal (aka "mathematical") logic part of mathematics? Now that's a philosophical question.

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.

reply
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.

reply
[dead]
reply
Yes, this. Comprehension is the point. We could map this to something like physics. If a man on a horse can shoot another man with a bow, empirically he makes correct predictions on gravity, wind and relative motion. But he can’t explain it. It’s not any different if your model has some “embodied” or demonstrable understanding; the model is not part of the discourse.
reply
deleted
reply
I’m not convinced.

In history, we made much more use of hitting things with bows than abstractly comprehending arrow flight.

reply
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.
reply
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.
reply
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?
reply
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.
reply
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.

reply
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.
reply
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!
reply
Mochizuki enters the chat
reply
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?
reply
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.
reply
I don't think Lean is as rigorous as you implied here.

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.

reply
Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
reply
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.
reply
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.

reply
Yes, you still need to be careful, especially if you have reason to think that the proof was from a malicious actor.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

(N.B. from August 2026)

reply
Sincere question, as a non-expert trying to situate your comment: are you a mathematician with experience in proofs?
reply
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.

reply
Mate you managed to provoke with this comment. But you know what you’re saying right?
reply
Math humans can use but not understand is called engineering. -- paraphrase of Bill Hammack, https://engineerguy.com

https://www.youtube.com/@engineerguyvideo

reply
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.
reply
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?
reply
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.

reply
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.

reply
This is relevant, but only after AI has solved all the open problems including Millenium problems. Until then, as AI keeps solving harder open problems, people will pay attention and be interested.
reply
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.

reply
We have thousands of years of precedent that suggests that breakthroughs in mathematics tend to accumulate into broader technology breakthroughs in other domains.

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."

reply
> 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.

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.

reply
And that's an issue why?

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.

reply
It could just as easily be the opposite: it could end up being far easier to reasonably direct and evaluate the research direction and output of AI systems than human mathematicians, who are forced to specialize over decades and essentially cannot pivot and often can't even meaningfully evaluate each other's work.

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.

reply
Moreover, the disdain you have for low-value output in mathematics is not unique to you

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.

reply
> I didn't say anything about low-value output.

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.

reply
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.
reply
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.
reply
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.

[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.

reply
Many eminent mathematicians did their best work while not talking about it with anyone, sometimes in isolation. Newton's calculus, Perelman's poincare, much of Grothendiek's work, Wiles's fermat, Ramanujan's earlier days. That's not all top mathematicians as you can look at Von Neumann as a sociable counter-example. But it shows that discussion of your current ideas is not a requirement. Grothendiek goes so far as to say it is a net negative for mathematical creativity because it is difficult to resist thinking like the herd without some level of seclusion.
reply
deleted
reply
[dead]
reply
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.

reply
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.
reply
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.

reply
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.
reply
> 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

reply
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.

reply
> 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

reply
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
reply
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?

reply
deleted
reply
I don't know, it sounds analogous to how the early Amish would have started their doctrine: "if the craftsman cannot do the task by hand, then they shall not use a machine ..."
reply
I was thinking about that too.

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.

reply
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.

reply
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?
reply
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.

reply
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.
reply
Just package the proof as a library and put it in some source code repository like github.
reply
deleted
reply
What if the result is a counter-example? A fact that disproves the conjecture? Is that not publication-worthy?
reply
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.

reply
> 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.

reply
> 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.

reply
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.
reply
I guess then the likely outcome is that nobody will get any more prestige from presenting new proofs. The fall of the theorem economy, as David Bessis says: https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...

Edit: I just saw Tao actually mentions the above essay in his paper.

reply
Tao has yet to produce work that outshines those whose work he studied and memorized. Not worth the reverence merely being a VHS copy of history.

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.

reply
wtf?! Tao is the only mathematician I can name, and widely considered the foremost living one.
reply
Says more about your own effort to learn math than Tao's ability.
reply
You should definitely inform the wikipedia editors as well https://en.wikipedia.org/wiki/Terence_Tao#Recognition .

(I don't know why you're so butthurt BTW - neigher of your ad-hominem comments actually outline your concern)

reply
It's right there in my initial post; barely any of the work is his own.

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.

reply
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.
reply
This artificially limits mathematics to the limit of human ability.

It should be ignored and refused.

reply
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

reply
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.
reply
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.
reply
[dead]
reply
deleted
reply