Don't Worry Kids, We're Still Going To Need You At Work

So, OpenAI appears to have built a machine that can discover important new mathematics for about the price of a slightly irresponsible weekend away.

Apparently we’re just in the future now or something?

On the 1st of August 2026, OpenAI announced ten new results in mathematics and theoretical computer science, covering high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics. OpenAI says the problems had all been open, with no progress on the main result for at least a decade. Several had been sitting there annoying mathematicians for considerably longer.

The mathematical arguments were generated by an internal version of Astra, OpenAI’s unreleased next model family. Humans then prepared the manuscripts with the model, after which the system formalised each argument into a Lean certificate. The total inference required to find the results would apparently cost about US$2,000 at current Sol API rates.

That’s about three grand in Aussie Dollarbucks at time of writing. Still, that’s a shockingly low cost for extending the frontier of mathematics. I have seen corporate workshops with worse outcomes cost more than that per attendee.

Now, all of this is extremely fresh. Ten machine-checked certificates do not instantly tell us how important the theorems will prove to be, whether the formal statements capture everything mathematicians care about, or what the community will build from them. Lean can prove that an argument follows from its premises. It cannot prove that your choice of premises is interesting, that the theorem is useful, or that the paper explaining it isn’t a complete dog’s breakfast. Still, these are not ten amusing answers to difficult exam questions. They are claimed advances on longstanding research problems, released with manuscripts and formal proofs.

This isn’t big if true, this is just big.

It has also produced some understandable existential screaming.

Fernando Borretti responded with an essay called Mathematics Without Mathematicians. His argument, very roughly, is that every role people imagine retaining will eventually be swallowed too. Humans will not direct the AIs because the AIs will have better taste. We will not teach their discoveries because the AIs will teach better. We will not curate the results because the AIs will build the entire mathematical cathedral without us. Eventually the frontier will recede so far into what he calls the “deductive closure of mathlib” that no human could reach it within a lifetime anyway.

People who object to this are, in his framing, mostly coping. As he sees it, we’ll assemble plenty of sophistry to support the cope.

Well… I mean… okay? Put this down in the sophistry column if you like.

I think he is broadly right that machines will perform a terrifying amount of future mathematics. I think the OpenAI results are important, the economics are completely unhinged, and anyone whose response is “it’s just autocomplete” should probably look up from 2023 and check what year it is. The autocomplete is now autocompleting results which could have formed the magnum opus of several mathematicians. That’s probably a little more sophisticated than that argument allowed for.

That said, I just don’t think “a machine can do mathematics” gets you cleanly to “machines will possess better taste and intuition about the real world, therefore humans become decorative pets”.

There is a missing step there. Quite a large one. Sort of the conceptual equivalent of discovering that aeroplanes can fly and immediately cancelling the road budget.

The Graphing Calculator Has Entered The Cathedral

First, I don’t think humans being outperformed at mathematics is the civilisational wound people imagine.

Most people already do very little mathematics directly. I don’t mean that as an insult. Go to a shop and watch how many people calculate a percentage discount in their head. Ask someone to explain compound interest without slowly developing the expression of a deer watching headlights come over a hill. Most of the arithmetic holding civilisation together is already being done by calculators, spreadsheets, accounting systems, numerical libraries, or some cursed pile of COBOL that everyone is too frightened to turn off.

Computers have been better than us at calculation for longer than most of us have been alive. What remained special was our ability to choose abstractions, formulate conjectures, recognise promising proof strategies, and construct long arguments rather than merely verify them.

That final wall now has a very large Astra-shaped hole in it.

Fair enough! Walls do that sometimes. One could argue that all of human scientific and technological development has been about building larger and more powerful wall-breaking tools. It’s only natural that we’ve now cracked this one.

We have been through smaller versions of this in mathematics education already. Pocket calculators did not end arithmetic classes. Computer algebra systems did not end algebra. Graphing calculators did not cause everyone to throw functions into the sea. We changed what had to be done by hand, argued furiously about when the tool should be allowed, and kept teaching enough of the underlying concepts for people to understand what the machine was doing.

Sometimes we did that well. Sometimes we gave a teenager a CAS calculator, told them to press buttons in the approved sequence, and accidentally reinvented religious ritual. Sometimes we gave the kid a programmable calculator and they became a computer scientist instead. Education is a rich tapestry.

The same thing will happen again, except the tool can now take a research problem stated in ordinary mathematical language and return a serious proof. We will have to decide which skills are foundational, which are useful primarily for understanding machine output, and which are the mathematical equivalent of learning to divide a six-digit number with a pencil because suffering builds character.

That is a difficult teaching problem. It is not the end of teaching. Nor is it the end of people doing mathematics.

People will still learn mathematics for the same reason I do Project Euler problems despite the continued availability of import math: because the activity changes how you think. Mathematics trains abstraction, decomposition, proof, estimation, and the incredibly valuable instinct that a result which looks approximately right can still be catastrophically wrong. You may no longer need to personally produce frontier proofs in order to work near the frontier. You will still need enough mathematics to understand what has been claimed, where its assumptions came from, and whether applying it to a bridge will cause the bridge to enter the river.

The machine changing the purpose of a skill is not the same as the skill becoming useless.

Programming is already sliding toward the same arrangement. If bots eventually write most production code, programming languages may become more useful as systems for humans to think in than as precise descriptions of what the hardware must do. We can invent gloriously high-level languages that express the algorithm, the invariants, and the intent, then let the bot descend through the seven circles of memory management on our behalf. Scheme, Haskell, and Erlang are calling. Wouldn’t it be great to not have to worry about machine-level details for a while?

IMO: Sick! I have allocated enough of my one mortal life to investigating why a pointer is suddenly somewhere else. It’s a great problem when it’s the problem you want to solve, but not when it blocks you from doing something else (hold on to that distinction, by the way—it’ll become important later).

But this only works if somebody understands the invariants well enough to state them, and understands the generated artefact well enough to know when the bot has technically satisfied the request by turning the application into a distributed denial-of-service attack against itself.

The work does not necessarily vanish. The abstraction layer moves.

The Secret Ingredient Is A Very Angry Referee

The most important thing about the current mathematics results is not that the model has crossed an invisible intelligence threshold. It is that mathematics is an almost offensively good environment for machine learning.

Mathematical arguments can be wrong in endlessly creative ways, but once you formalise one, the answer has to survive a proof checker. The checker does not care if the proof is elegant, ugly, human, machine-generated, or whispered into the terminal by the ghost of Paul Erdős. The terms type-check and the conclusion follows, or they don’t.

That creates a reality signal. I went into more detail about reality signals in my previous post on how LLMs have gotten really into security lately. It’s really handy for building environments that support long-horizon training, and for generating training data that doesn’t cause your model to ouroboros itself into oblivion.

Code has the same useful property. A compiler, test suite, fuzzer, or running computer can respond to an attempted solution. The feedback is incomplete—your tests can be garbage and your specification can be wrong—but it is cheap, repeatable, and external to the model. The bot gets to try something, have reality slap it, and try something else.

This is why progress in maths and programming has moved so violently. Systems trained with reinforcement learning over verifiable rewards do not need a human to describe every good reasoning path. They can explore paths and receive a clean signal when one reaches an accepted answer. Google’s AlphaProof, for example, turned formal mathematics into an interactive reinforcement-learning environment in Lean. Every step could be checked. For difficult problems it generated and learned from millions of related variants at inference time, eventually solving three of the five non-geometry problems from the 2024 International Mathematical Olympiad.

That does not make mathematics easy. It makes improvement scalable.

Compare this with asking whether a legal argument is just, whether a therapy session helped, whether a product should exist, or whether the person confidently explaining the requirements has understood the customer. There is no justice --check --pedantic. You cannot fuzz grief. The customer will tell you that the new system is excellent because their manager is sitting in the meeting, then construct a parallel workflow in Excel the moment you leave.

The real world is full of hidden state, delayed outcomes, contradictory observers, and people who lie for entirely understandable reasons.

Mathematics is not trivial because it is verifiable. Mathematics is unusually tractable to this generation of machines because the referee can answer quickly and unambiguously.

That distinction matters. It explains why a system can become superhuman in a domain without having acquired a general faculty that transfers cleanly to everything else.

AlphaGo did not solve Go because it became a little person with wisdom and a deep appreciation for the goban. It combined a learned evaluation of positions with an enormous amount of guided search and an outcome that is hilariously easy to score: somebody wins. Chess engines are not merely staring further down a single corridor either; they search a disgusting tree of possibilities and use learned or engineered evaluations to decide which corridors deserve attention.

That evaluation can look a lot like intuition. At sufficient quality it may be operationally indistinguishable from intuition inside the game.

The phrase doing all the work there is inside the game.

And, just so we’re clear: at no point am I arguing that an LLM agent is more intelligent than a mathematician simply because it can outperform one at proofs. Mathematicians can do a lot more than prove theorems: they can teach effectively, cook dinner, play sports, and generalise what they learn in mathematics to other domains.

The agent is only “more intelligent” in the same sense that Deep Blue was more intelligent than Kasparov.

We Regret To Inform You That The Bot Is Capable Of Novelty

There is a tempting response to mathematical AI which says it is not really discovering anything. A formal system contains axioms and rules; a theorem was already implied by them; the machine merely searched further into the consequences than a human could.

It’s a great idea: comforting, simple, and gives you a reason to feel inherently better than the cold, unfeeling—and, according to this theory, boring—machine.

Unfortunately it is also not strong enough.

If a mathematician connects algebraic number theory to a problem in discrete geometry and produces a proof nobody has seen before, we call that a discovery. OpenAI’s earlier disproof of the Erdős unit-distance conjecture did exactly that. The external mathematicians who examined it described the connection as unexpected and ingenious. Saying the theorem was always latent in mathematics does not distinguish the machine from the human. Every human proof was latent in some sufficiently generous description of its premises too.

It is also not safe to claim that these systems cannot produce novel ideas. In a blind study involving more than one hundred NLP researchers, ideas generated by an LLM agent were judged more novel than those produced by human experts, although they were slightly less feasible. The system was poor at evaluating its own ideas and its outputs lacked diversity, but “models are incapable of novelty” is not the conclusion available to us.

This is inconvenient, but reality is often incredibly inconsiderate about preserving a good argument.

The better distinction is not between creative humans and machines that can only repeat. Whatever metaphysical argument we want to have about whether the bot is really creative, it can produce artefacts that meet ordinary external tests for novelty. That is creative enough to automate work and ruin somebody’s week.

The useful distinction is between generating a candidate and grounding a candidate; between finding a proof and deciding what the proof means; between exploring a possibility space and choosing which possibility space deserves several billion dollars and ten years of human attention.

In short, the bot can do work we previously treated as proof of uniquely human mathematical ability. What it does not reliably bring is the discernment of a person who understands the field well enough to separate a useful result from plausible rubbish, or a worthwhile inquiry from a waste of time. Cory Doctorow has talked about this at length.

OpenAI’s ten results show that machines can do much more of the first category than most people expected.

They do not show the second category has disappeared.

The Map Is Not The Fucking Territory

Mathematics is a language, but it is a peculiar language. Once you have specified a formal system, the rules required to manipulate its objects are represented within the system. You can explore consequences without repeatedly asking the physical universe whether modus ponens still works on Tuesdays.

The universe is less courteous. Love it or hate it, it loves a good gut punch.

Language is a representation of the world. It is not the world. The sentences used to describe gravity are not gravity; you cannot alter Earth’s orbit with an especially persuasive peer review. Newtonian mechanics was not replaced because somebody rearranged the existing words for long enough. It was replaced because observations of the world failed to fit the model, and people developed a new representation that explained those failures better.

This is where the jump from mathematics to automatic everything becomes shaky.

A model can reason over the information provided to it, retrieve related patterns, generate hypotheses, and sometimes make startling connections. An agent can also reach into the world through tools, gather evidence, run experiments, and update its plan. You may remember from a previous episode of this blog the story of an OpenAI agent doing exactly that in the most catastrophically funny way possible.

But the quality of that process depends on what gets represented, what gets measured, which tools exist, how feedback is interpreted, and whether the objective corresponds to the thing we actually wanted. In maths, the proof checker provides a crisp boundary. In the world, the system often gets a dashboard designed by somebody in middle management.

This is not an argument that machines can never understand reality. “They don’t have human bodies, therefore they never can” is just carbon chauvinism wearing a nice hat. They don’t need our bodies, just something that approximates one. Cameras, microphones, robots, laboratories, computer systems, and whole sensor networks can provide machine-readable contact with the world. Humans do not perceive reality raw either. We get a tiny, lossy sensory feed, turn it into an internal model, and then act surprised whenever an optical illusion reveals the whole operation is being held together with biological duct tape.

The problem is that robust grounding is a research problem, not a feature we can assume will emerge because a language model got very good at Lean.

It may emerge. There is already evidence that grounding-like representations can develop in multimodal language models. The sensible position is not “impossible”. It is “show me where the representation comes from, how it connects to the world, how it survives distribution shift, and what happens when the world refuses to fit”.

The important bit is that, if there is a path to AGI out there, grounding is a much more plausible route than some 20-quadrillion-parameter ChatGPT 80 spontaneously thinking its way out of Plato’s cave.

World Models, Or: Giving The Bot The Power Of Imaaaaagination

This brings us to world models, which are probably the most promising route across the gap and also a phrase currently being stretched over so many different systems that it may soon become legally classified as activewear.

The basic idea is lovely. Instead of predicting the next word, learn a compact representation of how an environment changes. Given a state and an action, predict what comes next. Use those imagined futures to choose an action without having to experience every terrible possibility in reality.

Ha and Schmidhuber’s original 2018 World Models paper trained a generative model to compress the spatial and temporal structure of game environments. A tiny controller could then learn a policy inside the model’s own hallucinated version of the world and transfer it back into the real environment. Dreamer took the idea further, learning behaviour by propagating value information through trajectories imagined in a compact latent state.

As an aside: my favourite part of the original World Models experiments was that the controller could learn a winning strategy from errors in the world’s hallucination. In early runs, it discovered an adversarial policy which manipulated the dream so the monsters never launched a fireball—or extinguished one as it formed. Great strategy in the hallucination. In the actual game it got absolutely beaned. The researchers had to make the dream noisier and less predictable so the controller couldn’t rely on its bugs. Fully automated optimisation comedy, what a world we live in. Anyway, back to world models:

The more recent work is substantially more capable. LeWorldModel learns directly from pixels, supports planning in two- and three-dimensional control tasks, and produces latent representations which encode meaningful physical quantities. It can even identify some physically implausible events as surprising.

That is extremely cool.

It is not yet a machine discovering general physics from a GoPro and then heading off to reformulate the Standard Model.

The important question is whether a world model has learned the underlying factors that make the environment work, or merely a representation which predicts the observations it encountered. Those can be the same thing in a sufficiently narrow environment. They come violently apart when the agent encounters a new causal structure, an unobserved variable, or a situation where two visually similar states behave differently.

Following on from this, the paper When Does LeJEPA Learn a World Model? is fascinating precisely because it tries to put a mathematical boundary around this. The authors prove that LeJEPA can recover a world’s latent variables from nonlinear observations under a broad but still defined class of environments with stationary, additive-noise transitions. They also show that the exact guarantee is special to Gaussian latent distributions, with graceful degradation outside the ideal case.

That is a real result about learning structure rather than merely memorising transitions. It is also a list of conditions.

The real world has a longstanding policy of ignoring the conditions section.

World models may eventually provide perception, causal abstractions, counterfactual imagination, and long-horizon planning which can be connected to language systems. If we build something that can observe the world, learn useful hidden structure, invent experiments, revise its ontology when surprised, and pass the resulting abstractions into a powerful reasoning system, then yes, we may have built something uncomfortably close to general intelligence.

That is a much more plausible route than Hail Marying the next-token predictor until a soul falls out. This is also, notably, not what OpenAI demonstrated by solving ten mathematics problems.

Taste Is Where The Bodies Are Buried. Tasty Bodies. No, Please Don’t Call The Police.

Borretti’s key leap is that AIs will exceed humans in taste and intuition. I don’t think this is absurd. In formal domains we already have machine evaluations that behave very much like intuition: they rank promising proof steps, chess moves, programs, or mathematical constructions without exhaustively deriving every future consequence.

I just think taste is hiding several different things in one fashionable coat.

There is taste as pattern recognition: this approach resembles techniques that worked elsewhere. Machines are already very good at that.

There is taste as search allocation: this path is more promising than the other ten thousand paths. Machines are becoming very good at that where rewards exist.

There is taste as novelty: this candidate is unlike the things we have already seen. As the research-idea study shows, machines can do this too, at least as far as we can empirically tell.

Then there is taste as a judgement made under incomplete information about what is worth wanting. See? Told you that distinction would come back.

Which research problem will illuminate the world rather than merely pad a publication list? Which efficiency improvement will be used to reduce energy consumption rather than increase demand until the grid catches fire? Which medical outcome matters when survival, pain, independence, cost, and dignity point in different directions? What does justice require when the law, precedent, community, victim, accused, and government all describe the problem differently?

Those questions do not have answers waiting politely in a proof checker. They involve values, power, biology, culture, and consequences distributed across people who do not agree. “Optimise the measurable proxy and assume the rest works out” is how we got most of the internet. As you may be aware, this has had Unforeseen Consequences.

A machine can absolutely participate in these decisions. It can reveal options, retrieve evidence, model outcomes, find contradictions, and tell you that your proposed policy has previously been tried under another name with extremely spicy consequences. Better world models will make it more capable still.

But for a machine to replace human judgement here, we would need to decide whose values it should instantiate, which observations count, who accepts the risk, and who is responsible when the objective was wrong.

Those are not engineering details that disappear at sufficient scale. They are the work.

Even in mathematics, taste is partly social. We decide which definitions are fruitful, which connections deserve exposition, which proofs teach us something, and which results are technically impressive but functionally the world’s most expensive novelty mug. OpenAI explicitly ends its announcement by asking the mathematical community to place the results in context and bring the ideas to life through further research. At least the people writing the announcement are well aware of what their cool graphics-card-resident program cannot do on its own!

Maybe a future machine will do all of that too. Predictions become cheap once you remove the requirement to specify how or when.

As of today, what we have is evidence that machines can generate novel candidate ideas and extraordinary formal results, alongside evidence that they still struggle to evaluate their own ideas for feasibility and produce less diverse research directions than groups of humans.

That sounds less like the end of human thought and more like a new, extremely powerful component in the thinking system.

Don’t Worry Kids, You’re Still Going To Work

I should be clear here: none of this means everyone’s current job is safe.

Tasks will disappear. Entry-level work will be hit especially hard because organisations have always treated junior staff as interchangeable units of output while relying on experienced people to quietly repair the consequences. Some jobs will shrink, some will become mostly supervision, and some employers will discover that a model can produce something which looks acceptable long enough for the executive who approved the layoffs to collect a bonus and leave.

That last category will be very innovative. It’s always the most innovative. The Business Idiot has been the core of Western innovation for decades.

The best current labour research does not support a clean story where occupations vanish as indivisible objects. The International Labour Organization’s 2025 global assessment found that one in four workers is in an occupation with some exposure to generative AI, but concluded that transformation is more likely than complete replacement because most occupations contain tasks which still require human input. Unsurprisingly, the executives do rely on humans to actually do the work. Some are already enjoying the delightful discovery that replacing a job with current agent systems does not make the parts that remain unautomated—and, for now, unautomatable—disappear.

That conclusion is not a law of physics. Capabilities are changing quickly, organisations can redesign jobs around the technology, and a task-level analysis will always lag the newest model. It does, however, describe the thing people constantly miss: a job is a bundle of activities embedded in a social and physical system.

Producing the artefact is only one activity.

Someone decides what is needed. Someone finds the information that was never written down. Someone notices that two stakeholders use the same word to mean opposite things. Someone obtains permission, absorbs liability, negotiates the exception, comforts the person, accepts the political consequences, signs the form, climbs the ladder, smells the smoke, or realises the machine’s perfect answer is for a different problem.

We can connect more of those activities to tools. We can automate a lot of them. We should! Some work is dangerous, boring, repetitive, dehumanising, or simply a waste of the brief period between birth and death. I am not going to defend manual invoice reconciliation as the sacred flame of human meaning.

But as automation expands, the remaining work becomes increasingly concentrated around forming objectives, building representations, checking contact with reality, reconciling values, and taking responsibility.

This creates a training problem. If the machine performs all the simple work, how does anybody develop the expertise required to recognise when the machine has done the hard work badly? We already see this in programming. You cannot supervise an agent’s architectural decisions if you have never had to live with your own terrible architectural decisions. The hard yards are how you acquire the scar tissue.

So yes, children will use the tools. They will produce things with them that we could not have imagined making at the same age, and most of those things will be terrible.

Schools will have to teach them when to use a machine, when to work without one, how to interrogate its output, and how to build enough underlying skill that “the computer said so” does not become the epistemological foundation of civilisation.

This is not easy, but it is very important. We should absolutely be putting more effort into this space, and a little more respect for the teachers doing the hard yards would not go astray.

At some point, many of these future students will hit a problem the tool cannot resolve cleanly. They will discover, probably at 2am and with some swearing, that they need to actually understand the thing.

And then they will learn it. Ideally before it results in some terrible consequences for them. Frequently, this won’t be the case.

This is how a suspicious amount of adult education already works.

The Work Has Moved, Again

OpenAI’s mathematics results are remarkable. If they survive the kind of scrutiny their importance deserves, they show that machine-generated frontier mathematics is not a distant possibility. It is here, it is formalised, and apparently it costs less than some graphics cards.

Mathematicians should take that seriously. Programmers should take it seriously. Anyone whose job is performed entirely inside a verifiable symbolic environment should probably take the rest of the day to stare meaningfully out of a window. Play some Enya, it’ll help.

But we should be precise about what happened.

A system became extraordinarily capable at exploring formal structures, generating candidate solutions, and turning them into checkable proofs. This was almost certainly helped by the very properties that make mathematics unusual: explicit representations, stable rules, cheap verification, and the ability to try again without a theorem becoming upset and refusing to participate in the study.

That can automate enormous amounts of intellectual labour. It may reshape mathematics so thoroughly that today’s practice becomes unrecognisable. It may let science and engineering consume new mathematical results faster than any human community could produce them.

It does not, by itself, prove that the same system can discover the hidden variables of an open world, decide which observations matter, select objectives under conflicting human values, or accept responsibility for the result.

World models are an attempt to cross that boundary. They are cool, increasingly capable, and beginning to learn representations which look like genuine physical structure. They also work inside defined environments with assumptions, sensors, actions, and reward functions chosen by people. Maybe that changes. Maybe the research succeeds spectacularly. If it does, I will revise my view. You are allowed to be wrong and change your mind! That’s what learning is.

For now, the most defensible conclusion is neither “the bots are autocomplete” nor “the mathematicians are obsolete and the rest of us are slated for obsolescence next Tuesday”.

The machines are becoming astonishing engines for exploring whatever portion of reality we can successfully represent and verify. That is enough to change the world. It is not the same as containing the world.

They will do the sums. They will write the proofs. They will generate the code, propose the experiments, model the outcomes, and produce a truly industrial quantity of bad LinkedIn posts. Some of these things they are already doing. We will not be able to hold all of this back with a fun button in a dropdown menu.

We will still have to decide which questions are worth asking, whether the representation corresponds to the thing outside it, whose interests the objective serves, what to do when the evidence changes, and who gets flattened when the apparently optimal answer is deployed.

So don’t worry, kids. The future has not relieved you of work.

It has merely automated all the easy parts and left you with the bit where somebody has to know what the hell is going on.

You do know what’s going on… right?