数学家 Ken Ono 呼吁社区共建 MathEcon：经济学定理的 Lean 4 机器证明库
soumitrashukla9 · x · 2026-10-23
数学家 Ken Ono 转发宣传 MathEconLib 的发布：该项目将机器验证证明引入经济学理论，欢迎研究者深入其 Lean 4 代码库参与构建「MathEcon」。与另一条 Axiom Math 官方公告为同一事件，核心信息见该条摘要。
所属事件:Axiom Math 联手经济学家开源 Lean 4 经济学定理库 MathEconLib(3 条相关)→
「研究」频道最新
- 仅 1 克！无线微型显微镜实现自由活动小鼠全皮层单细胞成像 — KordingLab · 2026-10-23
- Mike Frank 抛出超导可逆计算难题:能否用无偏置约瑟夫森结凑齐 BARCS 通用原语集 — MikePFrank · 2026-10-23
- Arc Institute 用基因组语言模型绘制原核非编码序列图谱 — tedgreenwald · 2026-10-23
- 同行评审的 AI 化：审稿人终于「进入附录」了 — abursuc · 2026-10-23
- Anthropic 用 Claude 为 100+ 开源库写下汇编级安全形式化证明 — AnthropicAI · 2026-10-23
- 研究提出 9 种策略为多 LLM 协作选模型，最优可超随机 36.1% — shangbinfeng · 2026-10-23