北京
全球数学家每年产出数万篇论文，但能用计算机辅助验证的证明工具，对新手来说门槛高得吓人。一位曾参加数论定向阅读项目的开发者，决定改变这个现状。
她造了一个叫Starling的证明助手，核心目标只有一个：让初学者也能上手。不是另起炉灶做新系统，而是给已有20多年历史的Metamath语言，套了一层"人话"外壳。
Metamath是什么？一个极度极简的数学证明语言，特点是"逻辑不可知"——你可以用它写基于经典逻辑的定理，也可以写量子逻辑公理推导出的结论。代价是语法冷硬，像直接跟机器对话。Starling用JavaScript写了个编译器，把人易读的代码转成Metamath，同时继承后者庞大的已验证证明库和校验工具。
开发者坦承动机来自一次觉醒：数论项目让她意识到证明在数学发现中的核心地位。她开始追问：未来的证明长什么样？计算机辅助证明能否解决纸笔无法触及的问题？
历史给了她信心。19世纪对角线证明法的发明，催生了哥德尔不完备定理等里程碑；20世纪末，计算机首次完成四色定理的证明验证。她想知道：21世纪会不会属于计算机辅助证明？
目前Starling处于早期阶段，开发者正在招募用户访谈，目标是把"用户友好"做到底。她在项目文档里引用了两句诗：一句来自Ocean Vuong——"如果你发现自己身处黯淡世界，请记住身体内部向来如此黑暗"；另一句是Virginia Woolf的——"未来是黑暗的，而这正是未来最好的样子"。
工具已开源，支持导出为Metamath格式。对形式化验证或数学证明感兴趣的开发者，可以直接试用并反馈体验。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
