9 ms·

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

• czgov 1mo 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.
  • deleted 1mo ago
    [deleted]
  • ChadNauseam 1mo 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 1mo 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.
  • intuitionist 1mo 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 1mo 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?
  • akk0 1mo 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 1mo 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 1mo 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.
  • aleph_minus_one 1mo 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
• pfdietz 1mo 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.
  • cubefox 1mo 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 1mo 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.
      • cubefox 1mo ago
        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-economy https://davidbessis.substack.com/p/the-fall-of-the-theorem-e... Edit: I just saw Tao actually mentions the above essay in his paper.
  • BeetleB 1mo 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.
• kriro 1mo 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.
  • GPerson 1mo 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 1mo 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 1mo 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 1mo 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.
• mohamedkoubaa 1mo 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.
• tossandthrow 1mo 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
• nilkn 1mo ago
  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 1mo 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?
    • esafak 1mo 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.
    • cma 1mo 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.
    • nilkn 1mo 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.
• lacker 1mo 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 1mo 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 1mo ago
      Just package the proof as a library and put it in some source code repository like github.
      • Jblx2 1mo ago
        Apparently, it is Palomar: https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ https://terrytao.wordpress.com/2026/08/18/palomar-a-registry...
• _doctor_love 1mo 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.
• rowanG077 1mo 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.
  • chrisjj 1mo ago
    With no explanation, how will you know whether it genuinely is proof?
    • rowanG077 1mo ago
      A lean proof or equivalent. I should have been more clear.
• mlmonkey 1mo ago
  What if the result is a counter-example? A fact that disproves the conjecture? Is that not publication-worthy?
• odyssey7 1mo 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.
• raincole 1mo 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?
  • chrisjj 1mo ago
    Then with no way to prove the explanations, anyone can be a "mathematician".
• deleted 1mo ago
  [deleted]
• deleted 1mo ago
  [deleted]
• butwaitTheres4 1mo ago
  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.
  • unified101 1mo ago
    wtf?! Tao is the only mathematician I can name, and widely considered the foremost living one.
    • butwaitTheres4 1mo ago
      Says more about your own effort to learn math than Tao's ability.
      • unified101 1mo ago
        You should definitely inform the wikipedia editors as well https://en.wikipedia.org/wiki/Terence_Tao#Recognition 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)
        • butwaitTheres4 1mo ago
          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.
• brador 1mo ago
  This artificially limits mathematics to the limit of human ability. It should be ignored and refused.
• Otterly99 1mo ago
  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.
• amelius 1mo ago
  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 ..."
• addag 1mo ago
  [dead]
• jbstack 1mo ago
  I don't agree with this rule of thumb at all. Let's say tomorrow someone comes up with a formally verified proof that a major encryption algorithm underpinning the security of the internet can be trivially broken, but they can't explain it. You're saying it should be kept under wraps and not published? Tao is essentially saying that the only value in a proof is its ability to be understood, but that's wrong. A proof is also valuable because it establishes a new fact. The fact is useful in itself, even absent an explanation.
  • jumpman500 1mo ago
    I sort of agree, if you can guarantee the AI generated proof isn't a false positive. To be fair though, your example would be easy to explain to someone. You just show how the encryption algorithm can be trivially broken. A program that can break major encryption algorithm would likely be understandable, or at the very least we could show how it can decrypt things.
  • nixon_why69 1mo ago
    Tao is talking about academic publishing, based around learning for it's own sake. If no learning happened, do not publish. From a different angle, what we don't understand can absolutely hurt us and you're right too, but it doesn't contradict Tao's viewpoint. Edit: if you had a PoC cracking the encryption, I think the result is still publishable due to impact and the fact of the empirical result. That's different from some esoteric proof that nobody is even sure it's right.
  • applecoffeecake 1mo ago
    Tao is clearly referring to mathematics journals. Any kind of practically useful result can easily be published in an engineering or applied scientific journal.
  • feoren 1mo ago
    There has already been a formally verified proof of the Collatz Conjecture. The AI agent formally verified it by exploiting previously undiscovered bugs in Lean. The Collatz Conjecture is still unsolved. > Let's say tomorrow someone comes up with a formally verified proof that a major encryption algorithm underpinning the security of the internet can be trivially broken, but they can't explain it. You're saying it should be kept under wraps and not published? Absolutely. It could also be exploiting bugs in the verifier. Even if not -- even if that proof were correct and entirely written by humans, care should still be taken in how such knowledge is published. I'd want to give trusted parties a chance to try to fix the issue before letting it be known by black-hats, for instance.