形式化证明剖析
历史与综述
2024-11-20 v1 计算机科学中的逻辑
摘要
交互式证明助手使得普通数学家能够像使用编程语言一样，用形式化证明语言编写定义与定理，从而让计算机能够对其进行解析并根据形式化公理基础的规则进行检查。本文描述了使用证明助手工作的经验，并探讨了该技术将对数学产生的影响。
引用
@article{arxiv.2411.11885,
title = {Anatomy of a Formal Proof},
author = {Jeremy Avigad and Johan Commelin and Heather Macbeth and Adam Topaz},
journal= {arXiv preprint arXiv:2411.11885},
year = {2024}
}
备注
12 pages