Axiom Math 联合经济学家开源 MathEconLib：用 Lean 4 机器验证经济学定理
soumitrashukla9 · x · 2026-10-23
Axiom Math 与多位顶尖经济学家合作，正式开源 MathEconLib——一个基于 Lean 4 的经济学数学形式化共享基础库。
- 目标是为经济学研究提供机器验证的定义与可复用定理，覆盖微观理论（偏好、博弈、机制设计、一般均衡）、宏观理论（动态优化、异质性代理模型）与计量经济学（识别、估计、因果推断）。
- 研究者可用 AI 辅助形式化与证明开发，但数学架构由研究者决定，Lean 内核验证每个定理，并配有人工审查。
- 项目基于 Mathlib 构建，欢迎其他机构支持；核心贡献者包括来自哈佛、普林斯顿、多伦多大学等机构的学者（Scott Duke Kominers、Ken Ono、Bo Cowgill 等）。
「研究」频道最新
- 数学家 Ken Ono 呼吁社区共建 MathEcon：经济学定理的 Lean 4 机器证明库 — soumitrashukla9 · 2026-10-23
- IFM 开源 RL360:8192 并发沙箱、130 万 rollouts 的 RL 基建 — rupspace · 2026-10-23
- AI 揭穿阴谋论研究风波落幕：Science 撤回关注声明，结论不变 — DG_Rand · 2026-10-23
- Embodied First Exam：一行代码在 44 台机器人上考你的 Agent — ManlingLi_ · 2026-10-23
- Anima Anandkumar 演讲：AI 气象模型胜超算，但不会取代科学家 — AnimaAnandkumar · 2026-10-23
- GLM-5.3-Flash 实现 1M token 上下文训练，较基线提升 64 倍 — AndrewLBeam · 2026-10-23