What happened when I formalised an economics paper in Lean

Abstract

In September 2026 the Anthropic Institute published Economic Scenarios for Transformative AI, a task-based model of how AI might reshape the US economy by 2030. I spent two days formalising it in Lean 4 and building an independent solver, with no access to their code, which they do not publish. This essay reports what that exercise produced. Four things: a typographic ambiguity in the published equations that the paper's own results table resolves; an independent and deliberately incomplete reproduction, agreeing to within 0.35 percentage points on output and 0.6 points on unemployment while omitting one labour-market channel; the refutation of the criticism I set out to make; and a quantity the paper leaves as a word where a number was available. I also formalise a margin the paper explicitly excludes, and derive the point beyond which AI would make everyone better off while the national accounts recorded a contraction. The general lesson is narrow but I think real: formalisation is worth the trouble less because it catches other people's errors than because it catches your own.

What is proved, what is computed, and what is opinion

Before anything else, because the rest is easier to read against it.

flowchart LR
    subgraph P ["kernel-checked in Lean 4"]
        direction TB
        P1["the solve is <b>well posed</b><br/><i>a clearing rate exists<br/>and is unique</i>"]
        P2["the function bisected<br/>really is <b>monotone</b>"]
        P3["the thing reported<br/>really is a <b>share</b>"]
    end
    subgraph C ["computed, not certified"]
        direction TB
        C1["the <b>digits</b><br/>56.06, 2.08, 32.05"]
    end
    P --> G["<b>structure</b> guaranteed"]
    C --> H["<b>arithmetic</b> trusted"]
    classDef proved fill:#dcfce7,stroke:#16a34a,stroke-width:2px,color:#1a1a1a,rx:6,ry:6
    classDef comp fill:#fef3c7,stroke:#d97706,stroke-width:2px,color:#1a1a1a,rx:6,ry:6
    class P1,P2,P3,G proved
    class C1,H comp

The green side says the question is well formed and the answer is the answer to it. The amber side is ordinary floating point. Keeping the two apart is most of what honesty costs here.

No theorem in the paper was found to be wrong. Nothing below should be read as saying otherwise.

Why bother

The paper is good. Anton Korinek, Charles Jones, Szymon Sacher, Tess Cotter and Peter McCrory build a task-based automation model in the tradition of Zeira, Autor, and Acemoglu and Restrepo, bolt on a semi-endogenous growth block and a search-and-matching labour market, and run three scenarios to 2030. Their caveats section is unusually candid about what the model leaves out. This is not a paper crying out for correction.

It is, however, an unusually good target for formalisation, for a reason that has nothing to do with its quality. Appendix A prints the complete system, forty-four equations in forty-four unknowns, and Table 3 prints the answers. It ships no replication code. So you have a full specification and a full answer key, and nothing in between. That is exactly the shape of problem where you can find out whether you have understood something, because you can be told you are wrong.

My working thesis, which I have been pushing for a while across law, life logistics and software, is that natural language admits multiple interpretations, interpretations diverge as they propagate, and the cost of ambiguity compounds while the cost of formalisation is paid once. Economics papers are a good stress test. They are written in a hybrid of prose and mathematics where the prose frequently carries load the mathematics does not.

The first thing that broke was the typography

Proposition 1 gives the labour share in closed form. Extracted from the PDF, the equation reads, with the bracket ambiguous:

s_L,t = 1 - s_K,t0 + s_L,t0 [ ... ] e^{(1-sigma) dln r}

There are two readings. Either the bracket encloses only the summation, or it spans the base-period capital share plus the summation. These are different equations. Both reduce correctly to the base period when there is no AI, so the obvious sanity check does not separate them.

I could have emailed the authors. Instead I asked the paper. Taking the calibration from Table 1 and the rental rates implied by the published net returns, the two readings give:

Reading B reproduces all three. Reading A is wrong by up to twenty-six points. The 0.1 discrepancy on the extreme scenario is rounding in the published net return, which is given to one decimal place.

This is a small thing, and it is also the entire argument for formalisation in miniature. A human reader skims that equation and forms an impression. A formaliser cannot: Lean demands you commit to one parse, and having committed, you can test the commitment against something external. The ambiguity was invisible until something refused to accept it.

The second thing that broke was me

With the equations pinned down I built a solver. Not a transcription of theirs, which does not exist publicly, but an implementation from the printed system: build the logistic capability and diffusion paths from the mid-2026 anchors and the 2030 targets, solve the capital market by bisection, read off the results.

The first run looked like a disaster. The extreme scenario's GDP came out 10.9 percentage points above the published figure. That is not a rounding difference. That is a bug, and my first instinct was to go and find it.

It was not a bug. My solver computes the full-employment economy of section 2.1. Table 3 reports the full model, which also carries the monthly labour block and the ideas block. Those are different objects. Accounting for the two omitted blocks, using the paper's own published unemployment rates and ideas levels, the residual collapses:

Worst residual across three scenarios, 0.35 percentage points, from a clean-room implementation. I am fairly confident the model is understood.

The interesting part is that I had already made this mistake once, in the other direction, the day before. Equation 15 gives the employment target. Table 3 reports actual employment. I checked one against the other, found near-agreement on the two calm scenarios, and very nearly wrote down that equation 15 was validated. It was not. The extreme scenario showed a multi-point gap, and I read that gap as the search friction, which is the whole point of the labour block. Hold that reading lightly; it does not survive the next few paragraphs.

So within two days the same confusion produced a false positive and a false negative. Both times the cause was comparing two things that are not the same thing while their names suggest they are.

Then I did it a third time, and this one is worth the space because it is subtler. I recorded a prediction before writing the labour simulation: the target is −19.0 percent, the published actual is −21.5, so driving employment from the target must close a gap of 2.4 points, and that gap is the search friction. Writing it down first felt like good practice.

The prediction was mis-specified, because −19.0 is not the target. It is equation (19), the log-linear approximation the paper prints for intuition. The exact target is equation (13), in levels, and it gives −22.6 percent. The two forms agree to a tenth of a point in the modest scenario and diverge by five points in the extreme one, which is exactly where I was reading them.

With the right number the sign reverses. Published actual sheds less than target, not more:

That is what a lagging adjustment should look like, and it is consistent with the cognitive wage falling: work out the demand curve from the CES structure and cognitive labour demand is ℓ*_C · exp(−σ·g) in the wage discount g, so a wage at or below the common wage puts demand at or above target. Frictions hold employment up, not down.

Note what did the damage. Not a mistake in the model, and not a mistake in the arithmetic. I reached for the printed approximation because it was the legible one, and compared it to an exact published figure. That is the same error as the sigma one in the next section, which is also an approximation standing in for an exact form, and I made both before noticing either.

That is what a falsifiable prediction is actually worth. Writing it down first did not stop me being wrong. It meant that when the simulation ran, the disagreement was sharp enough to send me back to the definition instead of letting me nod at a plausible number.

The third thing that broke was my main criticism

Here is the part I did not expect to be writing.

Before building anything, I read the paper and formed a critique. The elasticity of substitution across task instances, sigma, is set to 0.5. That number is calibrated from an elasticity estimated across three broad occupation groups and then applied to an elasticity across task instances, which is a different object. The paper concedes estimates run from below one to above one. And sigma appears all over the place: twice in the labour-share equation, in the employment target, and nonlinearly in the closed form.

The paper runs robustness on the capital-supply elasticity and on wage rigidity. It does not run one on sigma. That looked like a gap, and I said so, with some confidence, on the grounds that above one the sign of the weak-link term flips.

Then I ran the sweep. Across sigma from 0.30 to 0.95, the 2030 labour share moves by 0.0, 0.1 and 0.7 percentage points in the three scenarios. It is very nearly sigma-invariant. My criticism was wrong.

The mechanism is worth stating because it explains the error. In the closed form the labour share is

s_L = 1 - (s_K0 + s_L0 * S) * exp((1 - sigma) * x)

and sigma sits in both factors with opposite effect. Raising sigma raises the inner sum, because the cost-decay term rises, and simultaneously shrinks the exponential. Measured on the extreme scenario the product varies by 1.05 percent over the whole range from sigma of 0.30 to 0.90, running between 0.5539 and 0.5597. Each factor separately moves by far more than that: the inner sum rises by about 60 percent across the same range.

flowchart LR
    S["<b>&sigma; rises</b>"] --> A["inner sum S rises<br/><i>because e<sup>-(1-&sigma;)a</sup> rises</i><br/>0.154 &rarr; 0.249<br/><b>+62%</b>"]
    S --> B["exponential shrinks<br/><i>e<sup>(1-&sigma;)x</sup></i><br/>1.125 &rarr; 1.018<br/><b>-9.5%</b>"]
    A --> P["<b>their product</b><br/>0.5539 &rarr; 0.5597<br/><b>+1.05%</b>"]
    B --> P
    P --> L["labour share<br/><b>barely moves</b>"]
    classDef up fill:#fee2e2,stroke:#dc2626,stroke-width:1px,color:#1a1a1a,rx:6,ry:6
    classDef down fill:#dbeafe,stroke:#2563eb,stroke-width:1px,color:#1a1a1a,rx:6,ry:6
    classDef out fill:#dcfce7,stroke:#16a34a,stroke-width:2px,color:#1a1a1a,rx:6,ry:6
    class A up
    class B down
    class P,L out

The two arrows into the product are what I missed. Each factor moves a lot; they move against each other, and what the labour share sees is only the residue.

The cancellation is a property of the exact closed form. It is invisible in the first-order expansion, where sigma carries a standalone weak-link term and looks consequential. I had reasoned from the linearisation, which is where the paper's economic intuition is developed and where the prose lives, and treated the linearisation's coefficient structure as evidence about the model underneath.

That is a specific, nameable failure mode, and I suspect it is common. Linearisations are published because they are legible. Legibility is exactly what makes them persuasive as a basis for reasoning they cannot support.

So the paper's decision not to report a sigma sweep is defensible for its distributional headline. What sigma does move is levels: extreme-scenario GDP runs from 41.6 to 49.1 percent above the no-AI path, and the average wage from 5.2 to 9.1 percent, across the same range. The wage nearly doubles. A band is warranted there, and the paper does not give one.

What survived: a word where a number was available

The result I would actually send the authors is small and, unlike my original complaint, correct.

The paper's most important structural insight, in my reading, is that at a fixed rental rate the wage tracks productivity, not displacement. Displacement moves the labour share and the demand for capital, and it reaches the wage only through the rental rate. So "AI takes jobs, therefore wages fall" is not a mechanism in this class of model unless capital is scarce. The wage falls only when capital is inelastic enough that the rental rate has to rise more than the productivity gain is worth.

Equation 12 makes that precise: there is a threshold capital-supply elasticity below which the average wage falls. The paper states that the wage rises in every scenario at their baseline of 3, and that it falls if the elasticity is "sufficiently small". It does not say how small.

It is a bisection away:

A margin of about 0.9 in the extreme scenario. Whether that is comfortable depends on how firmly the baseline is pinned, and here the paper's own reasoning is informative. The elasticity comes from Moll, Rachel and Restrepo, whose long-run wealth elasticity implies roughly 6. The authors halve it to 3, explaining that the original describes an economy taking decades to reach its steady state while theirs runs to 2030. That halving is a judgement, and it is the right direction of judgement, but it moves the parameter two thirds of the way from the literature value to the threshold. Halving it again, on the same reasoning applied to a shorter horizon, would cross it.

There is a second reason not to be relaxed. The parameter is a single homogeneous-capital elasticity standing in for the supply curve of compute, and over a five-year horizon those are different shapes. Fabrication capacity, grid interconnection and power availability bind hard for two or three years and then stop binding, which is a supply curve that is steep and then flat. A constant elasticity is the one functional form that cannot represent a bottleneck which resolves. The paper leans its choice upward precisely because compute is "financed in a world market and built in a year or two", which is an argument about the far end of that curve applied to the whole of it.

I am not claiming the wage falls. At their calibration it rises, exactly as they say. I am claiming that "sufficiently small" is doing work that a number would do better, and the number is 2.08.

The margin outside the boundary

There is one more thing, and it comes from the paper's own caveats:

We do not assign a value to AI's use in household production, which lies largely outside GDP.

Take that seriously and it has a sharp consequence.

All five of the paper's scenario primitives keep a task instance inside the market. Automation moves it to the firm's capital. Augmentation leaves it with the firm's worker. Reinstatement creates new market tasks. Every one is counted, because every one is a transaction.

There is a sixth possibility with no room in the model. The instance can leave the market altogether. The taxpayer stops buying an accountant. The parent stops buying tutoring. The small firm stops buying a paralegal's hours. The work still happens, the household is better off, and the transaction disappears, taking with it the expenditure that GDP is built from.

flowchart TD
    T["<b>A task instance</b><br/>AI is now capable of it"]
    T -->|"<b>&psi;</b> automation"| K["performed by the firm's <b>capital</b>"]
    T -->|"1 &minus; <b>&psi;</b> augmentation"| W["performed by the firm's <b>worker</b>,<br/>faster"]
    T -->|"<b>&rho;</b> reinstatement"| N["a <b>new</b> market task appears"]
    T -->|"<b>h</b> &nbsp;the sixth margin"| H["performed <b>outside the market</b><br/>by the household itself"]
    K --> C["<b>counted in GDP</b><br/>the transaction still happens"]
    W --> C
    N --> C
    H --> X["<b>not counted</b><br/>welfare rises,<br/>the transaction disappears"]
    classDef inside fill:#dbeafe,stroke:#2563eb,stroke-width:1px,color:#1a1a1a,rx:6,ry:6
    classDef outside fill:#fee2e2,stroke:#dc2626,stroke-width:2px,color:#1a1a1a,rx:6,ry:6
    classDef counted fill:#dcfce7,stroke:#16a34a,stroke-width:2px,color:#1a1a1a,rx:6,ry:6
    class K,W,N inside
    class H,X outside
    class C counted

Every route the paper models ends in the green box. The sixth ends in the red one, and the model has no arrow for it.

This margin runs in the opposite direction to every mechanism in the paper.

Writing h for the fraction of AI-performed instances that leave the market, and a for the log cost saving per instance, the arithmetic is clean enough to prove. Measured gain never exceeds welfare gain; the wedge between them is exactly the disintermediated mass scaled by one plus the gain; and measured output falls exactly when

h > a / (1 + a)

At the scenarios' own 2030 gains, that threshold is 23.1, 30.9 and 44.4 percent.

The proved threshold governs a first-order, TFP-like accounting object: the AI-attributable gain, md(1−h)a − md·h. It is not GDP. Run the same h through the whole model, where instances leaving the market also shrink the task mass the closed form operates on, and measured GDP crosses below its no-AI path considerably later, at h of 39.8, 53.7 and 65.0 percent. The general-equilibrium response cushions it: with fewer market tasks the rental rate falls back and the labour share recovers, which partly offsets the lost expenditure.

So the honest version is the later one. If more than roughly half of AI-performed instances leave the market in the substantial scenario, measured GDP is below where it would have been with no AI at all, while welfare is meaningfully above it.

There is a second effect I did not anticipate, and it cuts against the paper's headline rather than its level. Disintermediation raises the measured labour share, by 0.3, 2.0 and 8.0 points across the three scenarios as h runs from zero to a half. Work that leaves the market is disproportionately drawn from the automated instances, the ones capital performs, so removing them removes capital's share along with them. In the extreme scenario the accounts would record a labour share of 52.6 percent where the market-only model says 44.6. So a world with substantial off-market AI use would look, in the statistics, like a world where the labour share held up rather better than this model predicts, for reasons having nothing to do with workers doing better.

Two things this is not. It is not a criticism of the paper, which excludes household production explicitly and says so in the caveats. And it is not a criticism of GDP, which is doing exactly what it was designed to do. GDP measures market production. It has never claimed to measure welfare, and Kuznets warned against the conflation when he built it. Diane Coyle's history of the statistic is largely an account of people forgetting that. The problem is not that GDP is broken but that it is about to be asked a question it was never built to answer, by people quoting it as though it were.

I have also left out a second measurement channel that runs the same way. If AI raises the quality of a service at an unchanged price, real output growth is understated unless the deflator captures the quality change, and deflators have historically been poor at exactly this. That channel is additive to the one above and I have not modelled it.

The general point is old. Nordhaus and Tobin raised it in 1972, Marilyn Waring made it the centre of If Women Counted in 1988, and the BEA's own household satellite accounts put household production at 43 percent of GDP in 1965 and 28 percent in 2010. The nearest modern analogue is open-source software, where Hoffmann, Nagle and Zhou put the supply-side value at 4.15 billion dollars against a demand-side value of 8.8 trillion, a ratio of about two thousand to one. Free digital goods have the same shape: Brynjolfsson and co-authors' GDP-B work finds the internet's welfare contribution running at roughly 0.29 percent of annual US GDP in a period when GDP recorded it as close to nothing.

What is specific here is the threshold in this model's parameters. h is unmeasured, and I am not claiming it is large. I am claiming it is the quantity worth measuring, because we now know what value it has to exceed before the headline statistic starts pointing the wrong way. If AI's consumer surplus behaves anything like open source or free digital goods have, the measured GDP numbers in every scenario are the wrong object to be arguing about.

Objections

The four I would raise if someone showed me this.

"Two days is not long enough to understand a macro model, and your agreement with Table 3 is coincidence." Possible, but the failure modes point the other way. An implementation that agreed by luck would not also reproduce the labour-share figures to 0.04 points in the substantial scenario, nor recover the unemployment rate to 0.02 points, nor have its one disagreement turn out to be a rounding in the published calibration. Coincidence does not usually survive that many independent checks. What I would concede is that agreement on outputs does not prove agreement on mechanism, and my labour block demonstrably does not match theirs, since it omits a channel.

"You are quoting uncertified floating-point numbers while making a fuss about formal verification." Fair, and I have tried to label every number accordingly. The proofs constrain the structure: they say the solve is well posed, that the function being bisected really is monotone, and that the object being reported really is a share. They say nothing about the sixteenth decimal place. Making the numbers certified requires interval arithmetic with exponentials and logarithms, which needed a fix to the only Lean library that provides it; that patch is upstream and unreviewed. Until then these are ordinary numbers computed carefully, and I would rather say so than imply otherwise.

"Your measurement wedge assumes the disintermediated work is as valuable as the purchased service it replaces." It does, and that is the weakest assumption in it. If AI-assisted self-service is worse than the professional it displaces, welfare rises by less than the threshold formula implies, and the threshold is correspondingly too low. I would defend the direction and not the magnitude: the sign of the effect on measured GDP does not depend on the quality assumption, only its size does.

"Nobody disintermediates half of anything." Possibly not. But the open-source comparison is not reassuring: there the demand-side value exceeds the supply-side by roughly three orders of magnitude, and essentially none of that gap appears in national accounts. The point of the threshold is not that we will cross it. It is that nobody is measuring the quantity that would tell us.

What the formalisation actually bought

An honest accounting, since the point of the exercise was to test the method rather than the paper.

The kernel-checked Lean proofs caught nothing. Not one of the paper's theorems was wrong. The equations are right, the closed form is right, and the claim I most wanted to check, that the capital market has a unique clearing rate, is true and provable from the intermediate value theorem in nine lines. The proof does surface something the one-clause assertion hides: capital demand has three terms that move with the rental rate and the first of them is increasing, so monotonicity is not obvious until you substitute and watch a term cancel. But that is illumination, not correction.

What did the work was everything around the proofs.

Committing to a parse found the bracket ambiguity. Building an independent solver found that I had confused targets with actuals, twice, in both directions. Running a sweep refuted my headline criticism. A differential test between the Lean evaluator and the Python solver disagreed by 0.01 on one threshold, which turned out to be a rounded value in the published calibration: the stated 0.45 is a rounding of 0.448, and only one of the three scenarios is affected. Zeroing the AI shock entirely, to ask whether my labour market was stationary in the absence of any shock at all, found that it was not, and that a 0.41-point level error was propagating into every scenario. And extending the measurement wedge into the full model showed that a proved threshold I had reached for governs a first-order accounting object rather than GDP, which is the same target-versus-actual error a third time.

What it cost, since that is the other half of any claim about a method: two days, and a working knowledge of Lean 4 and Mathlib that took me considerably longer than two days to acquire. The reimplementation and the differential tests would have taken about the same time in Python alone. The marginal cost of the formal layer, given the skill, was perhaps half a day. The marginal cost of acquiring the skill is the real number and I am not in a position to quote it honestly.

Every one of those is a check on me. The formal layer's contribution was not proving the economics correct. It was refusing to let me proceed on an unresolved ambiguity, and giving me a structure rigid enough that my own errors had somewhere to show up.

That is a less heroic account of formal methods than the usual one. I think it is the more useful one. The value is not that the machine finds the flaws in other people's reasoning. It is that the machine will not accept the vagueness you would otherwise have carried forward in your own.

I want to bound that claim, because "formal methods caught my mistakes" is exactly the sort of sentence that detaches from its evidence and becomes folklore. This is one person, one paper, two days. Four of the five things listed above were caught by the independent reimplementation and the differential tests, not by the proof assistant, and you can build both of those without Lean. What Lean specifically contributed was the forced parse, which found the bracket, and the discipline of having to state what each object is before you can say anything about it, which is what surfaced target-versus-actual both times. That is a real contribution and a narrow one. I would not generalise it to a claim about formal methods in economics from a sample of one.

The Lean formalisation, the solvers, and the calibration with per-parameter provenance are in a private repository; I am happy to share them with anyone who wants to check the arithmetic. The numbers quoted are produced by ordinary floating point, not certified interval arithmetic. Making them certified requires a Lean library whose build I had to repair along the way; that patch is upstream at girving/interval and awaiting review.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.