Brian Albrecht on AI, EconLib, and the Future of Economic Theory
A recent Fortune article discusses Axiom Math’s EconLib project, which aims to use AI and formal verification to make foundational economic theory more precise. ICLE Chief Economist Brian Albrecht spoke to the publication about the promise and limits of using Lean-based tools in economics and antitrust analysis. Read the full piece here.
Brian Albrecht, a theoretical economist at the International Center for Law and Economics who works at the intersection of formal proofs and antitrust policy, has no affiliation with Axiom but uses Lean often in his work, especially with regard to antitrust law. The rise of AI tools has made it an “exciting time for economic theory,” he said, adding that something based on Lean for economic theory would “absolutely” be useful for his work. “There are a few people who have started to play around with it,” he said, adding that it would “allow people to build up on the work of others” and provide another angle to tackle big economic problems.
At the same time, Albrecht drew a sharp line between tightening theoretical foundations and winning real cases. “The big disputes in antitrust … aren’t about proving results in a model,” he said. They’re more about what’s the right market definition or who are the right competitors, and he didn’t think AI can be used to formalize this yet. He pointed to the ongoing Google search appeal as an example: “We’re parsing through the Microsoftdecision and what exactly the words mean.” That’s not really about proving the foundations of Aumann’s theorem correct, in other words.
Also, Albrecht said the verification burden is real — the “hallucination” problem. Even as AI helps fill in the steps, Albrecht said there is “just no way around needing different people to approve and verify” new results — though “Lean helps get us a long way there.”
Albrecht landed in almost exactly the same place. AI has turned him, he said, “a little bit more into a mathematician” — letting him formalize things he couldn’t pin down before because he lacked the pure-math training of a PhD. “That’s one more mathematician out in the world solving problems,” he said. “In a lot of ways it’s an exciting time.”