MathEconLib：用 Lean 4 构建机器可验证的数理经济学基础库

学术经济学家与 Axiom Math 于 2026 年联合发起 MathEconLib，基于 Lean 4 和 Mathlib 构建共享的形式化经济学基础库，提供可复用的定义与定理，覆盖偏好、激励、均衡、动态、识别、估计与推断等主题。