why mathema

The bottleneck moved.

When AI makes code cheap, understanding becomes expensive.

Across many technology teams there are two different kinds of software review culture. In one, pull requests are approved inside of thirty minutes and review is light-touch, focused on critical issues rather than opinions on smaller improvements. In the other, review is genuinely thorough (possibly too thorough) and pull requests can sit for three days while somebody senior works through what the change actually does, what it is supposed to do, and what might go wrong on the unhappy path. That makes the senior person incredibly valuable, and also a constraint on delivery speed. Both cultures can make sense, depending on their respective organisation, environment and maturity.

AI coding tools are adding a third culture, often without anyone choosing it: very little review at all, on the assumption that the model wrote the code correctly because it reads well and the tests it generated pass. It is fast, and for a prototype it can be the right call. In production it leaves two questions unanswered until the day something breaks, namely who is accountable for the outcome, and who understands what the code was expected to do well enough to say whether it failed.

Authorship and understanding used to come bundled

Here is the property of traditional development that is easy to miss, precisely because it was free. When somebody wrote code they produced several things at once: the implementation itself, evidence that they had understood the problem, a known person accountable for the design and its quality, context about the solution's limitations (in tests, documentation, comments, or simply someone to ask), and a small update to their own reputation. Organisations usually only ever paid attention to the first one.

That does not mean developers understood their code perfectly, because they plainly did not, and anyone who has inherited a system knows how thin some of that understanding was. But authorship and understanding were coupled. Whoever wrote a pricing model knew something about the model, and whoever designed a schema knew something about the business rules underneath it.

AI code generation unbundles that. A model can produce a perfectly plausible implementation without anyone in the loop holding the corresponding mental model, and the prompt that carries whatever intent there is gets discarded straight afterwards. This is not a completely new problem, since people have shipped code they did not understand for as long as there have been libraries, code generators and Stack Overflow. What is new is the scale and the cost: AI did not create the possibility of working without understanding, it made working without understanding cheap enough to become the default route to production.

The new bottleneck

AI can take the creation of a piece of software from days to minutes. It does nothing comparable for the time it takes to answer whether this is what was actually wanted, what it assumes, what happens when those assumptions fail, and how anyone would even know. Generation scales almost without limit and human attention does not, so as generation gets cheaper, establishing confidence becomes a larger share of human productive time, until it is most of what is left.

A proper review of AI-generated code tends to take longer than a review of human-written code. The reviewer starts further from the intent, looks at pull requests that can be substantially larger, can't shortcut the evaluation by relying on a colleague's track record, and has limited means of asking the author why decisions were made. So the gain is not the naive one, "AI writes code twenty times faster, so we are twenty times more productive", and realising a real increase means looking at the whole lifecycle, not just the writing.

Won't AI just review the code too?

If the author and the reviewer have made the same wrong assumption about what the code is for, more reading does not help, because neither is looking for the right thing. That is the real reason independent review works, namely that it is not another pair of eyes so much as another mental model, arrived at by a different route.

The same applies to generated tests. If a model writes the implementation and then the tests from the same reading of the requirement, the tests tend to confirm that reading rather than challenge it. It is like checking a translation by translating it back with the same dictionary: if the dictionary has an error in it, the round trip is perfectly self-consistent and perfectly wrong, and the consistency is exactly what stops anyone noticing. Those tests aren't worthless, since they catch things and prevent regressions, but evidence drawn from the reasoning that produced the code confirms less than evidence drawn from somewhere else.

And the cheapest source of trust the industry had quietly disappears. A reviewer who has worked alongside an engineer for years knows how careful they are and what kinds of mistakes they make; reputation is a form of compression, a prior that can be updated cheaply instead of re-deriving everything. Coding agents mostly don't carry that kind of persistent, accountable reputation today, and a model's confident tone is not evidence.

Accountability does not transfer to the model either. When generated code fails in production, the responsibility still lands on a person and an organisation, and so does the question of what the code was supposed to do in the first place. If nobody stated that expectation, nobody can say with confidence whether the failure was a bug, a misunderstanding or a case nobody considered, and the incident review starts from exactly the place the code review skipped.

The cost of producing code is falling. The cost of knowing that the code is correct is not.

Making intent the artefact

The rise of generative code development brings back an age-old problem under a different guise, namely that language is imprecise for defining intent, and the answer is to reach for something more mathematical. A sentence describing what a function should do cannot be checked, whereas a property quantified over a domain can.

If the diff is no longer reliable evidence of anyone's understanding, then reviewing the diff is no longer the right unit of work. The alternative is to make the intent itself the artefact: state what must be true about a function as a set of checkable claims over a declared domain. The claim says what should be true, the implementation says how it is achieved, and the evidence says why it should be believed, so the reviewed thing becomes a short list of statements in the language of the problem instead of a long diff in the language of the solution. That is Claim-Driven Development.

What mathema does about it

mathema is the System 0 engine for that loop. It checks each claim against the real implementation, proving it symbolically where the function lifts into algebra and running the real function against it where it cannot, and it always says which of the two applies. A falsified claim comes with the input that breaks it, and a proven one holds for every input in its declared domain, which is a very different statement from "the tests passed".

It also answers the question a platform lead actually asks, namely how good is this code, really. mathema reports three scores rather than one: implementation, how much of the code a test, a probe or a proof has reached; intent, how much of what the code is meant to do is explicitly specified and up to date; and clarity, how much of each function's behaviour its verified claims have pinned down (technically, a score from the behavioural entropy the claims remove over their declared domain, relative to what remains). Measured separately, a codebase with every line exercised and very little verified can't hide behind a test coverage number.

And it is independent evidence in exactly the sense above: for verifying claims there are no LLMs, no hallucinations and no token costs, and it runs on the developer's own machine. Agents can propose claims; they can't accept their own results, which stays a human decision.

The answer is not to use less AI. The generation savings are real, and this is the beginning of what's possible. The mistake is assuming that because code has become cheaper to produce, software has become proportionally cheaper to deploy properly. For decades a great deal of understanding came for free as a by-product of authorship, and that subsidy has ended. mathema is built to make understanding and review effective again.