AI가 경제 이론을 그럴듯하게 설명하는 일은 이제 낯설지 않습니다. 더 중요한 질문은 따로 있습니다. 경제학의 핵심 정리와 가정을, 기계가 검증할 수 있을 만큼 정확한 형태로 쓸 수 있을까요?
Axiom Math의 EconLib는 이 질문에 대한 실험입니다. 경제 이론의 기초 결과를 Lean으로 형식화해, 사람이 읽는 논문을 넘어 기계가 확인할 수 있는 라이브러리로 만들려는 프로젝트입니다.1
EconLib는 무엇을 바꾸려 하나
Lean은 증명을 코드처럼 다루는 형식 검증 언어입니다. 논리 단계가 맞으면 통과하고, 필요한 가정이 빠졌거나 모순이 있으면 통과하지 못합니다. 그래서 Lean에서 정리를 형식화한다는 것은 단순히 이론을 옮겨 적는 일이 아니라, 정의와 전제를 빠짐없이 명시하는 일에 가깝습니다.
EconLib가 참고하는 모델은 Mathlib입니다. Mathlib는 Lean으로 작성된 21만 개 이상의 형식 검증 정리를 담은 커뮤니티 유지 라이브러리로, 전 세계 수백 명의 수학자가 약 10년에 걸쳐 구축한 오픈소스 기반입니다.1
EconLib의 목표도 이와 비슷합니다. 경제학 지식을 단순히 모아두는 저장소가 아니라, 경제 모델의 정의·가정·정리를 재사용 가능한 검증 단위로 바꾸는 것입니다. Scott Kominers가 Axiom 팀과 함께 이 프로젝트를 공동 주도하고 있으며, 외부 경제학자도 기여하고 확장할 수 있는 공개 프로젝트로 설계됐습니다.1
핵심은 “AI가 증명했다”가 아니다
AxiomMathAI는 Robert Aumann의 Agreement Theorem을 Lean에서 형식화했다고 밝혔습니다. Aumann은 노벨상 수상 경제학자이며, 이 정리는 경제 이론과 의사결정 이론에서 중요한 위치를 차지합니다.
하지만 EconLib의 의미는 유명 정리 하나를 다시 증명했다는 데서 끝나지 않습니다. 더 중요한 점은 오래 쓰인 이론도 실제로는 여러 암묵적 전제 위에 서 있으며, 형식화 과정이 그 전제를 드러나게 만든다는 것입니다.1
경제학에서 이 차이는 큽니다. 이론은 논문 안에만 머물지 않고 시장 설계, 플랫폼 평판 시스템, 반독점 분석 같은 현실 판단과 연결됩니다. 어떤 결론을 정책이나 제도 설계에 적용하려면, 그 결론이 어떤 가정 위에서만 성립하는지 먼저 분명히 해야 합니다.
형식 검증이 해주는 일과 못 하는 일
EconLib가 제공할 수 있는 가장 실질적인 가치는 “모델 안의 논리”를 더 단단하게 만드는 것입니다. 정리의 결론이 주어진 가정에서 정말 따라오는지, 빠진 조건은 없는지, 다른 연구자가 같은 구조를 재사용할 수 있는지 확인하기 쉬워집니다.
그렇다고 현실 판단을 대신해주지는 않습니다. 예를 들어 반독점 사건에서는 시장을 어떻게 정의할지, 경쟁자를 누구로 볼지 같은 문제가 핵심 쟁점이 될 수 있습니다.2 이런 판단은 모델 내부의 논리만으로 해결되지 않습니다.
또 AI가 증명 작성을 돕더라도 검토 책임이 사라지는 것은 아닙니다. Lean은 많은 오류를 걸러낼 수 있지만, 어떤 정의를 채택할지, 어떤 결과를 EconLib에 포함할지, 그 형식화가 경제학적으로 적절한지는 연구자 커뮤니티가 판단해야 합니다.
EconLib를 볼 때의 기준
EconLib를 단순한 AI 성과 발표로 보기보다, 경제학 지식을 더 엄밀하게 축적하려는 인프라 실험으로 보는 편이 정확합니다. 앞으로 주목할 기준은 세 가지입니다.
얼마나 많은 경제학자가 실제로 기여하는가
어떤 기초 이론이 먼저 안정적으로 형식화되는가
법·정책·시장 설계에서 가정의 명료화가 의사결정 품질을 높이는가
EconLib의 가치는 AI가 경제학자를 대체하는 데 있지 않습니다. 경제학자가 서로의 가정을 더 정확히 공유하고, 검증 가능한 토대 위에 이론을 더 안전하게 쌓을 수 있게 만드는 데 있습니다.
1Exclusive: Economists have been teaching an unproven proof for 50 years. AI just solved it | Fortune
2Brian Albrecht on AI, EconLib, and the Future of Economic Theory
이 노트는 보도·비평·교육·연구 목적으로 작성되었습니다. 저작권 문의가 있으시면 에서 알려주세요.