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.

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.

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.

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.

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.

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.