大规模形式化证明对工作数学家的启示--来自ALEXANDRIA项目的教训
摘要：ALEXANDRIA项目是一个由欧洲研究理事会（ERC）资助的项目，始于2017年，旨在将形式验证引入数学中。过去的六年间，在数学形式化和一些相关技术，尤其是机器学习方面取得了巨大进展。六年的密集形式化活动表明，即使是依赖于多个数学领域的最先进成果，也可以使用当今可用的工具进行形式化。
作者：Lawrence C Paulson
论文ID：2305.14407
分类：History and Overview
分类简称：math.HO
提交时间：2023-05-26