nilkn

Autonomous software and hardware verification. They're just getting started. It's not just Axiom: Logical Intelligence, Harmonic, and a new one that just launched (&Truth). I suspect the business case is addressing the global cybersecurity crisis that AI is creating.

Making it cheap to do is probably exactly what they're trying to do. Formal proofs for verification take 10-20x as many lines as the core functional code being verified. Nobody's going to want to pay for 10-20x as many tokens at frontier pricing for verification unless they have to or it yields tremendous benefits. So getting the token price down as low as possible for a prover is probably a core part of the value proposition.

I understood them to be arguing that AI models are taking away the joy of certain things like mathematics but not producing commensurate value for humanity. We have a lower bound on twin primes, but that doesn't improve life for anybody, and the cost of getting the bound was removing human involvement from a lot of mathematical research, which was a source of joy for some portion of the human race. If all of this leads to curing major diseases without an AI takeover, it will have been worth it. But if it doesn't, then the ends don't necessarily justify the means.

You're trying to get me to make a claim stronger than what I'm making. The claim I'm making is that capabilities have moved since the paper's data (countless benchmarks support this), and it's not possible to measure the end-to-end effect of that inside industrial applications with complete access, adoption, and internal connectivity at the same pace. Therefore, the study is fundamentally out of date and conclusions about the present or future cannot be drawn from it unless you assume that technological progress cannot have affected the relevant outcomes, which is a strong assumption you'd have to back up separately. Note that the paper's model ties end-to-end outcomes to generated code quality and correctness which is precisely one of the variables that continues to move.

What the study actually shows is that organizations that had very little time to absorb older generations of a disruptive emerging technology experienced an indeterminate change in output (at the 12 month mark, anywhere from down 13% to up 25% -- the paper can't say where reality falls). It certainly doesn't establish any ceiling.

> I mention this because I've been hearing "Yeah, well, that opinion/study is completely invalid because it used a six month old tool. Today's release of SOMNOS 6.9 (Pinnacle Snoozytime) has totally changed the game!" every six months for what feels like the past five years now.

Given my own conclusion that it's not possible for conventional academic research to accurately snapshot industrial adoption of this technology, I would expect this pattern to continue for a while until either academia becomes much faster or technology progress slows down (or both). This just isn't yet a situation where you can rely on published papers telling you what to think -- you still need to mix in a bit of your own instinct and experience and extrapolation to get an accurate up-to-date read, even if there's some prediction error as a result.

I don't, actually. I can simply point out that its data is out of date, and then the numbers themselves are called into question without other numbers to compare them to. And that's what I did: I shared two arguments in two comments that converge on the shared conclusion that the paper's data is not up to date (or, more precisely, cannot be up to date).

I have my own experience to go off of, but this can also be inferred easily. There are many large corporations still working on "digital transformation" from 10+ years ago. There's no way such companies have fully onboarded and integrated frontier AI agents throughout their workforces with high adoption. The paper itself reports low adoption even after conditioning on access.

Everything did change after late 2025, but there are tiers of usefulness. Late 2025/early 2026 was the first time agents became clearly useful for personal projects. That's distinct from immediately having economically valuable end-to-end autonomous workflows in teams of median talent, which many would suggest is the threshold we've just recently crossed.

The data is still mostly 2025 and the 2026 data is mostly from the first few months, and most production deployments (at least in, say, the Fortune 500) lag the frontier by at least several more months (or much more). I suspect it's just not really possible for academic research at its conventional pace to offer an up-to-date perspective on this topic right now.

It's still the world's largest prison: most North Koreans would be killed on sight or imprisoned for even attempting to leave (i.e., escape). It also has millions of slaves, in fact the highest rate of modern slavery in the world (approximately the same as the US in 1860 before the Civil War). Kim Jong Un executed his uncle in 2013. Privilege or comfort, where it exists, can be stripped by force from an entire family at once for any reason. So, yes, Kim Jong Un is not a literal god on Earth -- there are balances he must maintain within the country to keep his power. Not every North Korean is a slave. You're not wrong about those things. But I feel your description is coming dangerously close to portraying it as a relatively normal country, which it most certainly is not. It is a prison and slave state, one of the most severe in history, enforced via extreme brutality and shielded by nukes against those who would save its people.

Like when it happened in 1637?

The answer to that depends on exactly how one defines writing. If by writing we mean full alphabets, etc., then no, but that is not the critical function that the word played in what I wrote. If by writing we mean encoding structured mathematical information physically (which today consists not just of written words/sentences, but also non-linguistic equations and computer programs) so that it can be accurately and unambiguously digested (and modified or corrected by) others, then yes: as far as we know there was no mathematical knowledge outside of spoken and bodily counting or the most basic visual symmetries of objects like stones or sticks.

Nope. We have evidence: what human mathematicians were producing and what AI systems are now producing.

As a response to my overall position, no, I think you threw out almost all of it.

On the question of a single word out of my entire position, that is a reasonably fair statement for mathematics (which is the topic under discussion). The fact that you think it's tautological supports both that you agree with its correctness and that this is a mostly irrelevant side conversation. And whatever you think the answer should be is not somehow not subject to the constraints of logic.

I don't know that any of this really matters. I could just as well say that you don't know anything at all about the internal experience of your dog's mind. All you can do is read behavioral patterns and attempt to make inferences. At best you have an approximation, and approximations tend to be wrong. Math is correct knowledge, not approximations of reality. Correctness is not a property of the idea or inference itself, since ideas and inferences can be wrong; it's the result of a verification process which you cannot possibly carry out in its entirety relating to the internal conscious experience of your dog.

We can dig into the philosophy of these definitions, but I think the far more interesting point is that even if we grant the existence of this kind of knowledge in the minds of human mathematicians, we have passed the threshold where that "knowledge" can keep up with systems that do not have access to it. Moreover, to claim humans have a "vast amount of mathematical knowledge" that is apparently valuable and that AI systems don't have, you'd have to prove that this "knowledge" is not implied or cannot be reverse engineered from the entire corpus of mathematical writing on which AI systems are trained. You'd also have to demonstrate that this "knowledge" leads to actual results that AI systems cannot generate without it. Given the results AI systems are producing, which are far beyond human ability at this point, it is more likely that AI systems have already internalized the entirety of this so-called "tacit knowledge" and then went much further, much faster, without humans in the loop at all.

I'd need to see specific examples. It's not clear to me that I'd consider this knowledge about the world but rather agreed upon conventions for how humans work together.

Those are simply called ideas, they are not unique to humans, and they are more likely to be wrong than right compared to anything OpenAI just produced. It would be bold and almost certainly spectacularly wrong to assume that multi-trillion-parameter AI models could not possess their own such ideas, generated during the training process as part of their internal model of the world. Beyond that, if we assume that such knowledge does exist in humans, its marginal value is clearly nearly zero now, as AI systems without access to it are vastly outperforming all human mathematicians combined by multiple orders of magnitude.

There is no such thing as knowledge that has never even been written down a single time by anyone or anything. Those are simply called ideas, they are not unique to humans, and they are more likely to be wrong than right compared to anything OpenAI just produced. It would be bold and almost certainly spectacularly wrong to assume that multi-trillion-parameter AI models could not possess their own such ideas, generated during the training process as part of their internal model of the world. Beyond that, if we assume that such knowledge does exist in humans, its marginal value is clearly nearly zero now, as AI systems without access to it are vastly outperforming all human mathematicians combined by multiple orders of magnitude.

I'm sorry but you don't actually need the mathematical community to check any of this. You just need autonomous verification, which already exists at scale and speed vastly beyond the entire human mathematical establishment. OpenAI simply rushed these out without completing that for every paper. These mistakes have nothing at all to do with the mathematical community and are 100% just the result of market pressure incentivizing speed at 1,000,000x the pace of human mathematicians. Frankly, a couple mistakes, trivially found not by humans but by humans using AI, is almost completely irrelevant. Human mathematicians have essentially nothing to contribute to this effort aside from prompting verification agents, which any of us can do if we cared to spend the time (most of us don't).

This is what everyone thought about modularity of elliptic curves. Then Wiles straight up just counted them (indirectly). You shouldn't be so confident about things that you do not know (since, if you knew them, you'd have solved the Riemann hypothesis!).

I don't know what you're trying to accomplish with this. I could just as easily say that you didn't engage with anything I wrote and just wrote an emotional and emphatic comment upset with me with no actual informational content whatsoever.

Have you considered the possibility that the AI labs could actually become more powerful than the US government precisely because they control this technology?

> Several hours of work with Fable simply convinced me it wasn't yet solvable and reinforced how hard of a problem it was.

This is the part that gives me the strangest feeling about it all, because you're not the only one with this experience. I've experienced this too on different problems, as have many researchers across many fields.

I disagree with the Fields Medalists on the majority of their complaints. AI math is happening and there's no going back. However, on one point I increasingly agree: virtually none of this stuff is possible with technology any normal citizen has access to. I have no problem with AI models making revolutionary advances in math or science. Where I start to have a problem is when the AI models making these advances are tightly withheld, proprietary, and seemingly never released with these capabilities intact. This has been the case for all of 2026 so far.

I suspect that this is in fact the source of much of the angst. None of this progress is reproducible outside of one or two teams inside OpenAI and Anthropic. It's becoming an incredible concentration of power that I don't know that we've ever quite seen before. Right now, it feels harmless because it's being used for wonky math problems that aren't (yet) practical for anything. But great power never stays harmless. History has taught us that countless times, in countless different forms.

You only need to trust your spec and the Lean kernel. If you trust those two things, you don't ever need to manually inspect or check the proof. That's the job of the Lean kernel, and your trust of it transfers over to trust of any proof verified by it.

Making sure your spec is correct -- and that it's expressed at a level of abstraction that both captures what matters, without overly constraining implementation details within the repo -- is the hard part. The more the spec constrains implementation details, the less you can ask an agent to, e.g., try many ideas to optimize a specific component without breaking correctness. And of course if the spec isn't enforcing what you wanted it to, then all the proofs don't count for much.

Some people say the spec issues are enough reason to avoid formal methods, but I'm not convinced. Part of me truly thinks AI formal methods is the future of a lot of software engineering. The basis of that belief for me is that the industry has collectively put almost no effort yet into solving the spec problem, and that's because for decades formal methods were too expensive to seriously consider most of the time. Now that AI is fundamentally shifting the economics, there's now, for the first time ever, a real incentive to try to solve the spec problem. And frankly it seems solvable to me; I view it as more of a product design and UI problem than a purely technical one.

This is coming next. There's nothing particularly special about theory building. Successful theory building is always oriented towards solving a problem, because otherwise even humans can easily spam out a bunch of nonsense. This is a real problem that the math community has experienced on multiple occasions pre-AI. I'd go further and say that theory building is irrelevant if it doesn't help solve problems people care about.

It's not survivorship bias, because math isn't a bunch of independent, parallel things, where one turned out to be useful and the rest was junk. There is no known way to advance only the portions of math that, centuries later, will turn out to be economically useful. Even with AI, we only know how to advance the entire subject.

You're effectively asking to predict the future hundreds of years in advance. Nobody and nothing can do that. With math, as with all science, you must be willing to accept that not everything will be a hit. There will be misses, and often the same person will generate both hits and misses, because it's fundamentally unpredictable what remains a miss and what doesn't over centuries. The best demonstration of this is that your own thinking here would've banned the invention of calculus: it didn't materially affect daily life for a solid century.

It'd cost you $30-$50 on AWS for a clean Lean build or maybe $100-$150 for the full verification suite. You are, in fact, capable of independently verifying the proof yourself if you don't trust all the people who've already done so.

I actually think it's the opposite: Lean proofs and autoformalization make it very easy to announce proofs alongside proofs of the correctness of those proofs (Lean certificates). It's not an absolutely fool-proof combination (the Lean kernel could still contain bugs), but it does immediately attach a very substantial degree of credibility to the result.

And that I think is essential to why some of the world's leading mathematicians are taking this so hard. In a world where we "merely" have AI systems capable of superhuman informal reasoning, verification, correctness, and acceptance could still only be conferred or anointed by human mathematicians. But a world that combines superhuman informal reasoning with superhuman autoformalization is a fundamental shakeup in the institutional order.

None of these incidents involve single instances of commercially or publicly available systems. They all involve large swarms of internal models. The stuff you're describing is not the research frontier. It's really not even close.

I think it's easy to infer that alignment of a single model does not clearly transfer over to alignment of a swarm of thousands of copies. Moreover, we're also seeing clearly that large swarms also unlock a step function change in capability, as a swarm can act like a complete research institution, spending thousands or millions of subjective hours of wall-clock thinking time just to deceive a single evaluator or crack a single math problem or design a single cyberattack.

I have a lot of respect for Tao and his peers. I studied math, but am not and have never been a practicing mathematician.

I sympathize with much of what Tao is saying, but I think the mathematicians behind this AI notice are demonstrating a predictable but clear lack of imagination.

First, let me explain where I agree and sympathize. Because they've spent their lives in a world where a relatively fixed set of grand challenges loomed large the entire time, shining as beacons to guide them, watching these problems be solved as side projects, with little effort put into extracting anything useful from the solutions, is without a doubt extremely demoralizing. Their role immediately shifts from "discover amazing solution and proof, then teach it to others and watch your discovery diffuse throughout the global community over years or decades" to "be handed an extremely dense inhuman solution and be one among many people attempting to understand, teach, and explain it, with nobody receiving any credit for anything." Mathematicians are, in general, not well paid. They do this for the love of it, the community, and frankly the credit. They didn't do it to just be explainers and digesters of automated outputs. They definitely don't deserve some of the ridicule I see them getting for struggling with this.

Now, let me explain why I still think this is the greatest advance in the history of math. Solving this current batch of problems does not mean math is solved. Not even close. There will be a "next" Riemann hypothesis. There will be deeper problems that cannot be solved even with a billion dollars of compute. Math already has vastly larger organizing principles than any of the Millenium problems, as represented in the Langlands program, which even with AI we have barely so much as touched. Riemann didn't even solve his own problem. He simply discovered it. His discovery of the problem is his greatest contribution. There's a chance for that today.

How about we get the Tao hypothesis? Or the Bhargava conjecture? How about we get the world's greatest mathematical thinkers together to sketch out what the next decade or two of AI-assisted mathematics should look like as a research program?

The work is either: (1) the act of concealment: generating an AI book that cannot be detected as AI generated; or (2) actually just writing the book yourself.

I think math is compressible structure. That's why we care about something like the Riemann hypothesis but, to use Tao's example, we really couldn't care less about computing the 10^10^10th digit of pi. The first compresses a vast amount of information about the primes, while the second decompresses information that we've already compressed (a few lines of code can define every digit of pi).

Most patterns that exist are incompressible. Math is basically a search for those compressions that do exist. An example I personally really like is the amplituhedron: a geometric structure that humans have just barely been capable of recognizing compresses information about scattering amplitudes and Feynman diagrams. That one happens to be within our reach, but it's right at the edge, and we can only imagine what glorious, wondrous compressions exist in abundance beyond the edge. Math accessible only to superintelligence would exist entirely beyond that edge, compressing patterns whose existence we cannot even detect using objects and constructions that we cannot grasp.

As an aside, I also think this is why AI is quickly becoming superhuman at math: intelligence is essentially a form of pattern compression.