Economics Has No Lean

AI produced a Lean-checked solution to Navier-Stokes. What would it solve in economics?

On Tuesday I read Tristan Buckmaster’s statement before I read the OpenAI announcement it was responding to. It is four pages long and I read it twice. The second time I was no longer reading it as news about mathematics. I was reading it as a preview of something that will happen to my own field, and the question was only which part. Buckmaster is a mathematician at NYU. For close to a year he and Levent Alpöge, who works at Anthropic, had been using AI models to chase proofs that solutions to the Euler and Navier-Stokes equations can blow up in finite time. The Navier-Stokes version is one of the seven Clay Millennium Problems. By August they had a result on the forced Euler equations, and a further result closer to the prize problem that is unpublished pending a Lean check. Then, according to Buckmaster, Sébastien Bubeck of OpenAI called to say that an internal model had already produced a hundred-page proof for forced Navier-Stokes, along the same narrow route Buckmaster and Alpöge had been following, and offered two options. OpenAI could publish the day after Buckmaster’s team, or Buckmaster could write up the paper alone and leave Alpöge off the author list, since Alpöge worked for a rival lab.

OpenAI denies the pressure. It also says it did not access either man’s private work, though it acknowledged it cannot rule out that de-identified data from their use of its products helped train the model. Terence Tao called the Buckmaster-Alpöge work a remarkable achievement. Four days earlier Anthropic had published a complete computer-checked formalization of Wiles’s proof of Fermat’s Last Theorem, written by Claude over eleven days. The credit dispute is what the coverage ran with, and it deserves the coverage.

The OpenAI proof came out of roughly ten thousand agents. They arrived at the argument after about 88 hours; formalizing and verifying it in Lean took another 17. That is a smaller detail than the dispute, and it is the one I kept returning to. Nobody has to trust OpenAI to know whether the derivation is right. Nobody has to trust Buckmaster either. Once the agents had produced the argument, Lean made the result cheaply and independently checkable. And that made me ask the question this essay is about. Suppose the same ten thousand agents were pointed at a question in economics. What would they be able to do, and what would they be unable to check?

What Lean actually checks

Let me be concrete about what Lean does, because the rest of the argument rests on it. A proof assistant does one thing. You state a proposition in a formal language, you supply a chain of inference steps, and the kernel either accepts each step as valid under the axioms or rejects it. There is no partial credit and no judgment call. The kernel does not know what the Navier-Stokes equations describe. It does not know what a fluid is. It knows the axioms and the rules of inference and nothing else.

This is what a verifier buys you: it separates generation from validation. You can generate arguments at whatever scale you can afford, with whatever mix of agents, heuristics and cross-pollination produces them, and then certify the survivor at low cost. The cost of a wrong candidate is a rejected formalization, not a retracted paper. Mathematics has that separation and most fields do not. The mathematicians who worried about the OpenAI result worried about credit, provenance, and whether a hundred-page proof nobody outside the company has read should count as public knowledge. The central technical question is no longer whether the derivation checks. Lean settles that relative to the formal statement. What remains open, and what the Clay Institute has not yet ruled on, is whether the formal statement the kernel checked is the problem as posed. That is a question about the specification, and I will come back to it.

So for economics the question is where the verifier lives and how far it reaches. I will be honest about my starting point. I assumed it does not reach very far, that causal inference is judgment all the way down. I had written as much in February. That turned out to be wrong in a specific way, and it is worth being exact about how.

The half of economics that is mathematics

Start with what I underestimated. Economics has two layers. One is a body of theorems. The other is a body of claims about the world that let the theorems apply. The first layer is exactly what Lean checks, and a surprising amount of it has already been checked.

Arrow’s impossibility theorem has had a machine-verified proof since Nipkow (2009) formalized it, together with Gibbard-Satterthwaite, in Isabelle/HOL. Existence of a mixed Nash equilibrium is a fixed-point argument. Brouwer’s theorem is far from a routine library lemma, but nothing in the argument lies outside what a proof assistant can check. If an AI lab announced tomorrow that its model had proved Arrow, the honest reaction would be that it had reproduced a 2009 result.

The analogy to Navier-Stokes lives in the open problems of economic theory: mathematical statements with no known general solution. Optimal mechanism design with more than one good is the cleanest example. Myerson (1981) characterized the revenue-maximizing auction for a single item. For two or more items there is no comparably simple, Myerson-style characterization. Daskalakis, Deckelbaum and Tzamos (2017) gave a duality condition that a mechanism is optimal if and only if it satisfies, which lets you certify optimality case by case without telling you what the mechanism looks like in general, and Hart and Nisan (2019) showed that when values across goods may be correlated, any mechanism with a bounded menu of options can capture an arbitrarily small fraction of the optimal revenue. This is a problem with a precise statement and no general answer. A model with a Lean backend could attack it the way it attacked fluid blow-up, and if it produced a result, the result would be checkable by anyone.

Let me bring this closer to what I actually do. The same holds for a class of identification problems. An identification theorem is a formal statement: given these restrictions on the joint distribution of observables, this parameter is or is not a function of that distribution. Magnac and Thesmar (2002) took the dynamic discrete choice model of Rust (1987), derived the exact degree to which it is underidentified, and showed which restrictions restore identification. Manski (1990) derived the bounds on a treatment effect that survive when you drop the selection assumption entirely. Every one of these is a theorem about distributions, and every one could in principle be stated and checked in a proof assistant. Weakening the assumptions of an identification result, or proving that a parameter cannot be identified under a given set of restrictions, is exactly the kind of task a prover with unlimited patience is suited to.

Even in macro, where “the identification problem” is usually said with a sigh, the formal core is algebra. A structural VAR is identified when the restrictions imposed on the impact matrix satisfy the rank conditions of Rubio-Ramírez, Waggoner and Zha (2010). Whether a set of sign restrictions produces an empty identified set is a question about a system of inequalities. Sims (1980) framed the problem as a choice among restrictions, but once a restriction is chosen, whether it identifies is not a matter of opinion. I went through the macro toolkit in an earlier essay; the point here is only that every method in it has a formal half and an argued half.

The standard account says mathematics has theorems and economics has judgment, so AI will transform the first and leave the second alone. That account undercounts the theorem layer of economics. It includes most of theory and a good part of econometrics. That layer is increasingly open to the same kind of automation that reached Navier-Stokes, and the credit disputes will look the same.

Where the verifier stops

Now the other side of the line. Lean cannot check the step before the theorem. The identification result for dynamic discrete choice tells you the parameter is pinned down if the unobserved state is conditionally independent of the observed one. It does not tell you whether that is true of the people in your data. The Manski bounds tell you what survives without a selection assumption. They do not tell you whether you should have made one. An instrument satisfies the exclusion restriction or it does not, and no proof kernel can establish from logic alone which it is, because it is a claim about how the world is wired rather than about the axioms of set theory.

Pearl’s framework makes the boundary visible. Given a causal graph and a query, the ID algorithm of Shpitser and Pearl (2006) is a mechanical procedure. It returns either an expression for the causal effect in terms of observables or a certificate that no such expression exists. That step is formally checkable. The argument lives in the graph itself. The arrows encode which variables you believe affect which, and which unobserved common causes you have ruled out, and nothing in the formalism can tell you whether you were right. Imbens (2020) gives the economist’s version of this worry: a graph looks precise, and the precision is borrowed from assumptions the graph cannot defend. Heckman (2008) divides empirical work into three tasks, defining the counterfactual, identifying it, and estimating it. The kernel reaches much of the second and the formal part of the third. It never reaches the first

.

Figure 1. Where the verifier stops. Verification proves correspondence to the specification, not correspondence between the specification and the world.

This is the point where the literature on language models and causality belongs, and it fits here better than where it is usually placed. It confirms the boundary, though not in the way its headlines suggest. Kıcıman et al. (2023) reported that large language models determine the direction of pairwise causal relationships with accuracies up to 97 percent on benchmark datasets, and argued from robustness checks that memorization alone does not explain the result. Zečević et al. (2023) offered the rival reading: the models recite causal facts embedded in their training text, and the paper calls them causal parrots. Wan et al. (2025) surveyed the field and found three uses: inferring graphs directly from text, correcting the output of statistical discovery algorithms, and supplying prior knowledge to those algorithms. To be clear, the interpretation of the benchmarks is disputed and I do not need to settle it. On either reading the model produces a graph, and on either reading nothing downstream can check whether the graph is true. When the literature the model learned from is right, it hands you the consensus at no cost. When the literature is wrong, it can reproduce the same mistaken consensus with considerable confidence.

So the ten thousand agents pointed at an economics question would do this. They would take the assumptions as given, derive every consequence, check every derivation, and produce an identified estimand or a proof that none exists. They would do it faster than any of us. They could also go looking for evidence on whether the assumptions describe Peru in 1990 or Denmark in 2015: institutional detail, pretrends, placebo outcomes, the historical record. What they could not do is certify that claim the way Lean certifies a derivation.

What changes anyway

None of this means the practice of empirical economics stays where it is. A large share of the hours in an empirical paper go into the verifiable layer, and that layer is getting cheap.

Consider the case I wrote about in March. Michael Wiebe spent three years replicating Moretti (2021) and found that the causal results were driven by code bugs: an event-study interaction that was never built, an instrument constructed from data that had not been sorted by city. Not one of those errors was a judgment call about identification. Every one of them was mechanical, and every one of them sat for years in a paper that funders had used to inform housing policy. I should be careful here, because the obvious reading of that case is wrong. A verifier does not reach the exclusion restriction. Would it have caught the sort command? Only if someone had first written down that the first difference was supposed to run within cities. A kernel checks that code does what a specification says. It has no opinion about whether the specification is the object the economist meant to build. Given the specification, the sort error is caught in seconds. Without it, a perfectly executed program produces exactly the wrong object and nothing complains.

Data construction is the second case. Dell and Rambachan’s 2026 NBER Methods Lecture is about estimation and inference when part of your data was produced by a model, and the reason the topic needs a lecture is that the practice is already common. Hypothesis generation is the third. Ludwig and Mullainathan (2024) built a tool that extracts candidate hypotheses from image data and hands them to a researcher for testing. Code and robustness are the fourth. Korinek (2025) shows working agents that run literature reviews, write and debug estimation code, and orchestrate a full workflow, with the caveat that choosing the question and judging the result still fall to the human.

Each of these can compress work that once consumed days or weeks of a research assistant’s time into hours. None of them changes the price of the assumption. Parallel trends cost the same to defend whether the event-study code took a week or a minute. If anything the assumption gets more expensive in relative terms, because it is the one input whose supply does not expand

.

Figure 2. Schematic, not an empirical estimate. AI reduces the cost of many research inputs, but much less so for choosing and defending the assumptions. Their relative price therefore rises.

One last thing, and this one is a guess. My suspicion is that the profession has rewarded methods that look verifiable. A regression discontinuity is legible in a way a structural model is not, and I think legibility has been paid for in placements and publications. The Navier-Stokes result puts a question under that reward structure. If a machine will do the legible part of a paper, the scarce part of the contribution increasingly becomes the part that was never legible: the argument that the world is arranged the way the graph says, and the argument that the object you told the machine to build is the one the question required. Those are the same step seen at two scales. A kernel is only as good as the proposition it is handed, and economics hands it propositions about the world. Economics has no Lean for that step. It never did. What the last week made clear is that everything else is on the table.

Further reading

Anthropic (2026), “Formalizing Fermat’s Last Theorem.” The computer-checked formalization of Wiles’s proof, and a clear statement of what a formalization is and is not.

Daskalakis, C., Deckelbaum, A., and Tzamos, C. (2017), “Strong Duality for a Multiple-Good Monopolist,” Econometrica 85(3), 735-767. The duality characterization of optimal multi-good mechanisms, and the closest thing economics has to an open Millennium problem.

Hart, S. and Nisan, N. (2019), “Selling Multiple Correlated Goods: Revenue Maximization and Menu-Size Complexity,” Journal of Economic Theory 183, 991-1029. Shows that bounded menus can lose almost all revenue with two goods, which is why the multi-good problem has no simple answer.

Heckman, J. (2008), “Econometric Causality,” International Statistical Review 76(1), 1-27. The three-task division of empirical work that maps onto what a verifier can and cannot reach.

Imbens, G. (2020), “Potential Outcome and Directed Acyclic Graph Approaches to Causality: Relevance for Empirical Practice in Economics,” Journal of Economic Literature 58(4), 1129-1179. Why economists distrust the apparent precision of a graph.

Kıcıman, E., Ness, R., Sharma, A., and Tan, C. (2023), “Causal Reasoning and Large Language Models: Opening a New Frontier for Causality,” arXiv:2305.00050. The benchmark results on pairwise causal direction that started the current debate.

Korinek, A. (2025), “AI Agents for Economic Research,” NBER Working Paper 34202. A hands-on guide to building research agents, useful for seeing exactly which parts of the workflow automate and which do not.

Ludwig, J. and Mullainathan, S. (2024), “Machine Learning as a Tool for Hypothesis Generation,” Quarterly Journal of Economics 139(2), 751-827. The clearest statement of what machine learning can do before the causal question is even posed.

Magnac, T. and Thesmar, D. (2002), “Identifying Dynamic Discrete Decision Processes,” Econometrica 70(2), 801-816. An identification result stated as a theorem, with the degree of underidentification computed exactly.

Manski, C. (1990), “Nonparametric Bounds on Treatment Effects,” American Economic Review 80(2), 319-323. Four pages that show what survives when you make no selection assumption at all.

Myerson, R. (1981), “Optimal Auction Design,” Mathematics of Operations Research 6(1), 58-73. The single-good characterization that the multi-good problem has failed to generalize.

NBER (2026), Methods Lecture: Melissa Dell and Ashesh Rambachan, “Estimation and Inference with AI-Generated Data.” The econometrics of treating model output as data.

Nipkow, T. (2009), “Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite,” Journal of Automated Reasoning 43(3), 289-304. The machine-checked proof of Arrow’s theorem, and evidence that the theorem layer of economics has been formalizable for years.

OpenAI (2026), “On the Navier-Stokes Millennium Prize Problem.” The announcement, with the writeup and the Lean formalization.

Rust, J. (1987), “Optimal Replacement of GMC Bus Engines: An Empirical Model of Harold Zurcher,” Econometrica 55(5), 999-1033. The original dynamic discrete choice model and the conditional independence assumption that later work would interrogate.

Rubio-Ramírez, J. F., Waggoner, D. F., and Zha, T. (2010), “Structural Vector Autoregressions: Theory of Identification and Algorithms for Inference,” Review of Economic Studies 77(2), 665-696. The rank conditions for global and exact identification of SVARs, which is the formal half of the macro identification problem.

Shpitser, I. and Pearl, J. (2006), “Identification of Joint Interventional Distributions in Recursive Semi-Markovian Causal Models,” Proceedings of AAAI, 1219-1226. The complete algorithm that decides, from a graph alone, whether a causal effect is identified.

Sims, C. (1980), “Macroeconomics and Reality,” Econometrica 48(1), 1-48. The paper that turned macro identification into a question about which restrictions to impose.

Wan, G., Lu, Y., Wu, Y., Hu, M., and Li, S. (2025), “Large Language Models for Causal Discovery: Current Landscape and Future Directions,” Proceedings of IJCAI 2025, 10687-10695. The survey that sorts LLM-causality work into its three uses.

Zečević, M., Willig, M., Dhami, D. S., and Kersting, K. (2023), “Causal Parrots: Large Language Models May Talk Causality But Are Not Causal,” Transactions on Machine Learning Research. The main skeptical interpretation of results such as Kıcıman et al.’s 97 percent figure.

Earlier essays: On Causality, Why Macro Never Had a Credibility Revolution, The Missing Sort Command.