No Fixed Frame Is Enough

Mathematics is producing proofs faster than it has ever produced them, and mathematical progress has not accelerated. That fact is not a paradox. It is the clearest available evidence for a structural claim about artificial intelligence — one that can be stated precisely, proved in three independent ways, and, uncomfortably, does not say what most people want it to say.

The Puzzle in Front of Us

In the summer of 2026, mathematics is experiencing something it has no precedent for. In May, an OpenAI model disproved the unit distance conjecture, an eighty-year-old problem of Erdős in combinatorial geometry. DeepMind systems resolved nine further Erdős problems with substantial autonomy. In July, a model proved the cycle double cover conjecture, open for more than half a century. And on the twentieth of July, Levent Alpöge posted a single short polynomial map that refutes the Jacobian conjecture in every dimension above two — a problem posed by Ott-Heinrich Keller in 1939 and listed by Stephen Smale among the great problems for the twenty-first century.

The natural inference is that mathematics is accelerating. Terence Tao, watching more closely than almost anyone, reports that it is not. He decomposes mathematical work into three activities — generating a proof, verifying it, and digesting it, where digestion means understanding a result well enough to contextualize it, explain it, and build on it. Artificial intelligence and formal verification have accelerated the first two dramatically and left the third roughly where it was. The result is what he calls an impedance mismatch: mathematics has moved from an era of proof scarcity to an era of proof abundance, and its infrastructure and culture have not adapted. His most striking observation is the one I want to build on. The enormous acceleration in proof generation has not produced a corresponding acceleration in mathematical progress.

Why not? If proofs are the product, and proofs are now cheap, the frontier should be racing forward.

The answer, I will argue, is that the frontier is not made of proofs. It is made of the frames within which questions can be posed at all — and those frames are produced by digestion, which nothing has made cheap. This is a specific instance of a general structural fact about lawful systems, one that can be established formally rather than gestured at. The general fact is that no fixed explanatory standpoint is ever sufficient. Not for a mathematician, not for a model, not for any system whatsoever.

That last clause is where this essay parts company with most of what has been written on the subject, including some of what I have written myself. The formal results are real, they are stronger than the usual hand-waving about creativity, and they do not establish a human advantage. They establish something more useful.

The Deficit Is Not Where We Think It Is

The common intuition is that AI is good at working with what is known and bad at reaching into what is not. It constructs from knowns and deduces from knowns. It operates in positive space. It does not reach into negative space — the unformed region where a genuinely new idea has to come from.

The intuition is pointing at something real, but the diagnosis is one layer off, and the layer matters.

Generating novelty is trivial. Raise the sampling temperature on any model and you obtain an unbounded supply of things nobody has ever said. Almost all of it is garbage. The hard part was never producing the strange thing. The hard part is recognizing that this particular strange thing is worth two years of your life, before anything exists that could confirm it.

Once you state it that way, the evidence rearranges itself. Consider where AI has in fact gone deep into unexplored territory. AlphaGo’s move 37, which no strong human player would have made and which was correct. AlphaFold, which solved a problem that had resisted fifty years of structural biology. AlphaTensor, which found matrix multiplication algorithms better than the best known human constructions. FunSearch, which produced genuinely new mathematical objects through program search.

Every one of these has a property in common, and it is not architectural. Each operates in a domain with a cheap, automatic, unambiguous oracle. Go has win and loss. Protein structure has RMSD against ground truth. Matrix multiplication has arithmetic correctness. FunSearch has a program that either runs and scores or does not.

Where a cheap verifier exists, machines search negative space better than we do. Where it does not, they revert to interpolating what has already been written.

This reframes the whole question. The bottleneck is not novelty generation. It is novelty evaluation in the absence of a verifier. And that is precisely what the word “intuition” has always been used to name.

What “Intuition” Actually Names

Intuition is not one capacity. It is at least four, with radically different prospects under continued AI progress, and conflating them is how the discussion stays vague.

1. A learned value function over unverified states

This is the grandmaster’s feeling for the right move, the one she cannot justify. It is real, it is not mystical, and it is not a human moat. It is a value function trained by delayed reward over many thousands of episodes. AlphaZero has one and it is better than ours. Chess and Go intuition — the inarticulate structural feel that gets cited most often as evidence of human specialness — was the first thing to fall. Any argument that leans on the grandmaster is leaning on a lost position.

2. Ambient sensing

Researchers are embedded in a continuous stream of signal: hallway conversations, half-finished preprints, the tone of a seminar question, what three different groups are quietly stuck on. This shapes judgment enormously and it is often mistaken for something occult — reading the zeitgeist, sensing where the field is going.

It is neither occult nor precognitive. It is latency and bandwidth. A working scientist sits inside a live causal loop with a world that has not been written down yet. A trained model reads a delayed, filtered, text-serialized snapshot of that same world. Being early means having sensors others lack. That advantage is real, and it is eroding quickly as agents acquire live data access.

3. Taste as compressed private failure

This one is underappreciated and I think it is the most actionable.

The corpus these models train on is the published record. The published record is the success-filtered subset of what was attempted. Nobody writes up the approach that felt promising for three months and quietly died. Nobody publishes the question that seemed too stupid to ask, or the calculation that came out boring, or the analogy that turned out to be superficial.

A senior researcher’s gut is a value function trained almost entirely on that unpublished record. She knows what dead ends smell like because she has personally walked down several hundred of them. Models have essentially none of this data. It is a difference in training distribution, not in metaphysics — which makes it falsifiable, temporary, and immediately actionable for anyone building discovery systems. The system that keeps a rigorous archive of what did not work, and why, will have an edge nobody else has.

4. Problem-finding

This is the genuinely open one, and it is not the same activity as problem-solving.

Solving is search within a specified space. Finding is constructing the space: choosing the representation, deciding what the objective is, drawing the boundary around what would even count as an answer. Optimization theory has a great deal to say about search and nothing whatsoever to say about where the objective function comes from. There is no loss function for having chosen a good loss function.

The empirical literature supports the distinction. Getzels and Csikszentmihalyi’s study of art students found that problem-finding behavior predicted later career success better than technical skill did. And the evolutionary computation literature has been circling the same point for fifteen years: Lehman and Stanley showed that objective-driven search is systematically deceptive, because the stepping stones toward an ambitious goal usually do not themselves look like progress toward it. Rewarding novelty rather than goodness sometimes outperforms rewarding goodness.

So: of the four, one has already fallen, one is eroding, one is a fixable data problem, and one is genuinely open. It is worth knowing which is which before making claims about what machines cannot do.

Three Theorems, One Shape

Now the formal core. Three results, from three unrelated areas of mathematics, converge on a single structural claim. Their independence is what makes the convergence worth taking seriously.

Self-reference: no model contains its own diagonal

Lawvere’s fixed-point theorem, published in 1969 and neglected for decades, shows that Cantor’s diagonal argument, Gödel’s incompleteness theorems, Tarski’s undefinability of truth, Turing’s halting problem, and Russell’s paradox are all instances of one result about cartesian closed categories. Yanofsky later restated the whole thing without category-theoretic language, which is where most people now encounter it.

The pattern: if you have a parameterized family of maps and a function without fixed points, the diagonal is never a member of the family. Something always escapes the parameterization.

I have proved a general version of this for self-models, machine-checked in Lean 4: for any parametric self-model and any fixed-point-free function, the diagonal is never a row of the model. No computability hypothesis, no arithmetic hypothesis. It holds for every type and every self-modeling architecture. No system that models itself can contain a complete model of itself.

Generation: no fixed framework closes the tower

The second result is my own Novelty Theory, and specifically the self-transcending generator theorem, also machine-checked.

There exist finitely specified, fully deterministic generators such that: one fixed law produces every phase of an infinite tower; each phase has an adequate explanatory regime; each successor regime conservatively preserves what its predecessor got right; each successor is genuinely irreducible to its predecessor; and no fixed explanatory standpoint drawn from the admissible class is ever the last word.

Nothing mysterious happens. The law generates everything. And still no fixed framework finishes the job. Explanatory closure is not entailed by lawful generation — a conclusion that overturns an assumption so widespread most people do not notice they hold it.

Measurement: compression cannot see across regimes

The obvious response to all this is to propose a better metric. Compression is the natural candidate — minimum description length as a principled measure of what counts as a real discovery. Schmidhuber built a formal theory of creativity on exactly this, defining interestingness as the first derivative of compression progress.

It fails, and the failure is instructive.

Minimum description length presupposes a fixed description language and, more damagingly, a fixed encoding of the data. You must already have decided what the observables are. But regime change routinely alters the carving rather than the bits. Fossils before and after Darwin are the same fossils; what changed was what counted as a feature of them. MDL scores hypotheses against a fixed observable set and is structurally incapable of scoring a change to that set.

The empirical version is worse. Genuine regime shifts frequently increase description length locally. Copernicus was not simpler than Ptolemy at the time of writing. Early quantum mechanics was uglier than the classical mechanics it displaced. Compression pays out only after the new regime has been developed and extended — many expensive steps downstream. Greedy compression progress is therefore deceptive in exactly Lehman and Stanley’s sense. Compression is a lagging indicator of a good frame.

The shape

Three results, three domains, one conclusion:

Fixedness is the disqualifying property. Not siliconness. Not the absence of interiority. Fixedness.

Notice what this does to the standard scaling argument. A trained model’s weights are a fixed reducer — an explanatory stance frozen at a training cut. The claim is not that the model is too small. A larger model is a larger fixed reducer, and fixedness is what disqualifies it, not size. Scaling arguments become non-responsive rather than merely unlikely to work.

It also unifies two things that looked separate. A verifier is a fixed adequacy predicate. Anti-closure says no fixed adequacy predicate covers the tower. So the oracle-dependence identified earlier is not a contingent engineering gap you close by building better oracles. What counts as adequate is itself regime-relative, and the regimes do not terminate. The verifier problem and the closure problem are the same problem.

The Concession

Here is where I have to say something that cuts against the conclusion many readers will want, and against the emphasis of some of my own earlier writing.

None of these results distinguishes humans from machines. All three are symmetric.

A human cognitive frame is also a parameterization, and the diagonal escapes it too. A human’s current explanatory stance is also fixed at any given moment. Diagonalization constrains every representational system equally, and there is no exemption clause for carbon.

The temptation to spend Gödel on human exceptionalism has a name — the Lucas–Penrose argument — and it has been refuted repeatedly by Putnam, Boolos, Feferman, and Shapiro, on a point that is simple once seen. The Gödel sentence of a system S is knowable as true only given knowledge that S is consistent. You cannot verify your own consistency any more than a formal system can. The incompleteness results therefore yield exactly zero asymmetry. Torkel Franzén’s Inexhaustibility remains the best treatment of what these theorems do and do not license.

I want to flag a second inference I am declining to make, one that appears in my earlier essay on the twist. There is a distinct argument that consciousness has a topology no representational system can achieve — that recognition requires an inside, and models have none. Grant that argument entirely and it still does not deliver the conclusion at issue here. Whether there is something it is like to change a frame is one question. Whether a frame change gets produced is another. The first is about interiority; the second is about capability. This essay concerns the second, and the argument from interiority does not reach it.

What the theorems actually do is relocate the question, precisely and usefully. The capability that matters is not the quality of a regime. It is the ability to transition between regimes. And that is a mechanism question. Mechanism questions are, in principle, engineerable.

The Escape Is Already Known, and It Is Mechanical

Diagonalization tells you where the obstruction is. It also tells you how to get past it, and the method is nearly ninety years old.

In 1939, Turing published “Systems of Logic Based on Ordinals” — the first systematic attempt to overcome Gödelian incompleteness by iterating the adjunction of statements, such as the consistency of the current system, that ought to have been accepted but were not derivable within it. The iteration can be continued into the transfinite. Feferman developed the theory substantially in 1962 with his transfinite recursive progressions.

You never reach closure. That is guaranteed. What you get instead is an unbounded generator of new frames, in which the diagonal at each stage is exactly what fuels the next stage.

The diagonal is not a wall marking where machines stop. It is the fuel supply.

Two honest caveats, because a proof theorist will raise them. Feferman and Spector showed the same year that completeness fails along paths in these progressions — the ascent is not a free lunch, and results depend sensitively on how ordinal notations are chosen. Franzén’s later survey is the careful modern treatment. Ordinal ascent does not hand you everything. It hands you unboundedness, which is what the argument requires.

Read this way, a genuine conceptual breakthrough has a mechanical description. It is a regime transition that is conservative over everything previously established and irreducible to the incumbent framework, triggered by something the incumbent cannot reach. Under that description, breakthrough-generation is not gated on interiority. It is gated on three architectural capacities:

Locating your own diagonal — detecting where the current frame fails rather than smoothing over the failure.
Extending rather than applying — treating the current frame as an object that can be modified, not only as the lens through which everything is seen.
Grounding the extension in something outside the frame — empirical contact, cost, consequence, other agents who disagree.

The third is where the honest residue of human advantage lives, and it requires no metaphysics at all. The ascent step needs a source of constraint the frame does not contain. Humans have that continuously and unavoidably, because we live somewhere and things happen to us. A frozen model has it only when a person supplies it. That is not a categorical difference. It is a missing feedback loop, and missing feedback loops get built.

It is worth noting that pieces of this have been attempted. Schmidhuber’s PowerPlay accepts a new self-invented problem only if the system still solves every previously solved one — which is the conservativity condition, implemented in code. What it lacks is the irreducibility condition. Half the specification has existed for over a decade.

Back to Mathematics: The Thesis in the Wild

Return to the puzzle we started with, because the proof abundance crisis is this entire argument playing out at the scale of a discipline, in public, right now.

Proof generation is positive-space work, and it just became cheap. Digestion is regime work: folding a result into a frame such that the frame changes and new questions become askable. That is exactly the conservative-but-irreducible transition described above, performed by a community rather than an individual.

Which explains the puzzle. The volume of results is exploding, but the frontier — the boundary from which new questions get posed — advances only through digestion. A backlog of undigested proofs does not move the frontier. It grows the inventory. Tao’s observation that generation accelerated while progress did not is the single best empirical evidence for the structural claim, and it is being generated in real time.

The Jacobian counterexample is the perfect specimen. The map is short. Independent verification came within hours, and the arithmetic was checked and documented by multiple parties working separately — one reduction produced a twenty-four-variable homogeneous cubic form with a nilpotence certificate, cross-checked by two independently implemented exact verifiers. The generation took a session. The verification took hours.

And the digestion is still open. Nobody yet has a conceptual account of why this particular map works — a result you can check but cannot yet understand. On the seminar thread where the verification happened, one participant said what everyone was thinking: he would like to reconstruct some story of how a person should have known to look there. Mathematicians are now doing that reconstruction in public, in a comment thread, offering geometric arguments and generalizations. That is digestion, visible, and it is the expensive part.

One qualification, because it matters and the headlines have blurred it: the counterexample refutes the conjecture for every dimension above two. The two-dimensional case, closest to the historical question, remains open. And it has not been through journal peer review.

Why Formalization Solves the Easy Half

The obvious institutional response is more machine-checkable formalization: make claims verifiable, build agentic peer review, require reproducibility artifacts. I believe all of this and I think it will happen. Someone is already drafting the protocols.

But it is important to be clear about what it does and does not fix.

Formalization solves validity. It does not touch worth. Lean will tell you a proof is correct and will say nothing whatsoever about whether the theorem matters. And validity is the easy half.

In one respect formalization makes the situation harder. A verified-correct but worthless theorem is more difficult to dismiss than an unverified one, because it arrives carrying a certificate. The failure mode is not a flood of wrong results. It is a flood of certifiably true irrelevance — cheap to produce, awkward to argue with, and perfectly indexed. The bottleneck does not settle at verification. It moves straight past verification to significance, where, by the anti-closure result, there can be no fixed adequacy predicate at all.

There is, however, a partial answer, and it follows from the same analysis that killed compression as a global metric.

Measure significance relationally

Do not ask whether a result compresses the world. Ask what it changes about what else becomes reachable. In a formalized corpus this is computable today:

By how much does this lemma shorten the proofs of other results in the library?
How many previously disconnected components of the dependency graph does it join?
Which downstream statements become decidable that were not before?

Run that over a formal library and you have a genuine measure of structural leverage — not a proxy for taste but a real quantity. This is the natural extension of agentic peer review from validity to worth, and as far as I know nobody has built it. Lehman and Stanley made an early attempt at quantifying impressiveness in an artificial-life setting; the problem deserves a serious second pass now that formalized mathematics gives it a substrate.

A useful asymmetry

One more practical point that the recent results make vivid. Refutation formalizes cheaply; proof does not. The Jacobian counterexample verified globally within hours because a counterexample is a finite object you simply check. A thousand-page affirmative proof is not.

The slop risk is therefore asymmetric, concentrated almost entirely on the affirmative side. Near-term, the highest-yield and lowest-risk use of these systems is refutation — searching for counterexamples, where verification cost is near zero and the epistemic exposure is minimal. Infrastructure design should exploit that asymmetry rather than treat all claims uniformly.

What the Anxiety Is Actually Tracking

There has been a great deal of visible distress among mathematicians, and it is easy to read it as wounded pride — a fear that the glory of a big proof is being taken away. Some of it is that. Most of it is something better.

In June 2026, sixteen mathematicians, computer scientists, philosophers and historians published the Leiden Declaration on Artificial Intelligence and Mathematics, which drew over a thousand signatures within a day and an endorsement from the International Mathematical Union. It defends five things: proof and certainty, attributable authorship, transparent and independently verifiable argument, shared standards of evaluation, and the autonomy of the discipline. Its concrete recommendations are about disclosure, retention of human responsibility for correctness, proper attribution, and refusing to let announcements substitute for review.

Read carefully, this is not nostalgia. Credit in a research field is not a vanity mechanism. It is the attention allocation function — the way a community decides where scarce effort goes. That system was calibrated to reward generation. Generation is now cheap. So the allocator has stopped tracking value at precisely the moment when allocation became the binding constraint.

Tao’s own prescription is the same diagnosis from the other direction: prestige needs to shift toward the people who verify and digest, and the community should stop treating a raw undigested proof as a finished result. The distress is a correct signal about a broken function, not a complaint about lost laurels. It deserves to be met on those terms.

What the Mathematics Actually Gives Us

Let me state the conclusion plainly, including the part that is unwelcome.

The negative-space deficit is real, and it is now grounded in three independent formal results rather than in intuition about creativity. But every one of those results indicts fixed frames, not machines. There is no theorem here that gives humans a moat, and anyone who tells you otherwise is misreading Gödel in a way that has been corrected for sixty years.

The asymmetry that currently exists between human and machine discovery is architectural and contingent, not categorical. Humans run an unbounded, badly instrumented, low-throughput regime-generation process, powered by confusion and by having something at stake. Current models are extremely capable frozen reducers with no such process at all. That gap is enormous today. It is not guaranteed by any theorem.

What the mathematics gives us is not a moat. It is a build specification, and a surprisingly specific one:

Locate diagonals. Instrument where the current frame stops paying — where residuals remain incompressible as data accumulates. A frame that is failing does not announce itself with a better competitor; it announces itself by ceasing to earn. That is a computable proxy for confusion, and it is available before a replacement exists.
Ascend rather than apply. Treat the current frame as an object. Build the transition operator, not just a bigger frame.
Ground the ascent externally. The extension step needs constraint the frame does not contain. Without it, ascent is just drift.
Archive the failures. Later regimes disclose structure in earlier phases that was not expressible at the time. A dead end is not waste; it is a phase awaiting a frame that can read it. Discarding failed branches destroys exactly the substrate that retroactive understanding operates on.
Score novelty properly. Not distance in embedding space, which rewards noise. Conservativity plus irreducibility: preserves everything certified so far, and decides something the incumbent provably cannot.

Keats called it negative capability — the capacity to remain in uncertainties and doubts without any irritable reaching after fact and reason. Stripped of the romanticism, it is a precise engineering requirement: the ability to hold an unresolved representation without collapsing it to the nearest known one. Models trained to produce fluent, confident, in-distribution continuations have had exactly that capacity optimized away. They resolve ambiguity instantly toward the nearest attractor. They cannot occupy I do not have a concept for this as a stable state.

That is a design flaw, not a metaphysical boundary. Which is the more interesting conclusion, and the more useful one, and — I think — the true one.

References and Further Reading

Diagonalization and self-reference

F. William Lawvere, “Diagonal arguments and cartesian closed categories,” Category Theory, Homology Theory and their Applications II (1969), 134–145.
Noson S. Yanofsky, “A universal approach to self-referential paradoxes, incompleteness and fixed points,” Bulletin of Symbolic Logic 9:3 (2003), 362–386. DOI 10.2178/bsl/1058448677.
Nova Spivack, Representational Incompleteness: Why No Self-Model Can Capture Its Own Diagonal. Lean library: representational-incompleteness-lean.
Nova Spivack, NEMS Paper 54 (observer non-self-exhaustion). DOI 10.5281/zenodo.19429831.

Explanatory anti-closure

Nova Spivack, Self-Transcending Generators: Fixed Causal Laws Without Final Explanatory Closure. DOI 10.5281/zenodo.19423547. Lean archive: DOI 10.5281/zenodo.19423148.
Thomas Kuhn, The Structure of Scientific Revolutions (1962).

Ordinal ascent

A. M. Turing, “Systems of logic based on ordinals,” Proceedings of the London Mathematical Society, ser. 2, vol. 45 (1939), 161–228.
Solomon Feferman, “Transfinite recursive progressions of axiomatic theories,” Journal of Symbolic Logic 27:3 (1962), 259–316.
Solomon Feferman and Clifford Spector, “Incompleteness along paths in recursive progressions of theories,” Journal of Symbolic Logic 27 (1962), 383–390.
Torkel Franzén, “Transfinite progressions: a second look at completeness,” Bulletin of Symbolic Logic 10:3 (2004), 367–389.
Torkel Franzén, Inexhaustibility: A Non-Exhaustive Treatment, Lecture Notes in Logic 28 (2004).

Against the Gödelian argument for human exceptionalism

Solomon Feferman, “Penrose’s Gödelian argument,” Psyche 2 (1995).
Stewart Shapiro, “Incompleteness, mechanism, and optimism,” Bulletin of Symbolic Logic (1998).

Novelty, objectives, and compression

Joel Lehman and Kenneth O. Stanley, “Abandoning objectives: evolution through the search for novelty alone,” Evolutionary Computation 19:2 (2011), 189–223. DOI 10.1162/EVCO_a_00025.
Joel Lehman and Kenneth O. Stanley, “Beyond open-endedness: quantifying impressiveness,” Proceedings of ALIFE (2012), 75–82.
Kenneth O. Stanley and Joel Lehman, Why Greatness Cannot Be Planned (2015).
Jürgen Schmidhuber, “Formal theory of creativity, fun, and intrinsic motivation (1990–2010),” IEEE Transactions on Autonomous Mental Development 2:3 (2010), 230–247.
Jürgen Schmidhuber, “POWERPLAY: training an increasingly general problem solver by continually searching for the simplest still unsolvable problem,” Frontiers in Psychology (2013).
Peter Grünwald, The Minimum Description Length Principle (2007).

AI in mathematics and the sciences

David Silver et al., “Mastering the game of Go with deep neural networks and tree search,” Nature 529:7587 (2016), 484–489.
Alex Davies et al., “Advancing mathematics by guiding human intuition with AI,” Nature 600:7887 (2021), 70–74.
Alhussein Fawzi et al., “Discovering faster matrix multiplication algorithms with reinforcement learning,” Nature 610:7930 (2022), 47–53.
Bernardino Romera-Paredes et al., “Mathematical discoveries from program search with large language models,” Nature 625:7995 (2024), 468–475.
Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang and Melanie Matchett Wood, “Remarks on the disproof of the unit distance conjecture” (2026).
“The new counterexample to the Jacobian conjecture,” Secret Blogging Seminar, 20 July 2026.
Agentic Publication Protocol: An Attempt to Modernize Scientific Publication, arXiv:2606.27386.

Proof abundance and community response

Terence Tao, posts on proof scarcity and proof abundance, Mathstodon, April–May 2026. Living summary: teorth.github.io/tao-web/ai-views.html.
Leiden Declaration on Artificial Intelligence and Mathematics, 2 June 2026 (16 authors, led by Jim Portegies; endorsed by the International Mathematical Union).
“Mathematicians issue warning as AI rapidly gains ground,” Science, 2 June 2026.

Problem-finding

Jacob W. Getzels and Mihaly Csikszentmihalyi, The Creative Vision: A Longitudinal Study of Problem Finding in Art (1976).