Astra 逼近经济学定理自动形式化,研究员押注 2027 年前攻克千禧难题

Afinetheorem · x · 2026-09-04

Afinetheorem 评价 Astra 在自动形式化（autoformalization）上已非常接近可用,包括经济学领域,并给出三点判断:1) 学术期刊（如 AEA，他去年已建议着手准备）很快应要求投稿附形式化证明;2) 构造性数学（constructive math）时代将至,他仍押注 2027 年前 AI 解决一个千禧年大奖难题;3) 数学的意义不止于形式化验证。