QED宣言

QED宣言是一项关于建立一个基于计算机的所有数学知识的数据库的建议，该数据库是严格形式化的，所有证明都是自动检查的。(Q.E.D.在拉丁语中是quoderatdemonstrandum的意思，意思是要证明的东西）。

这个项目的想法产生于1993年，主要是在RobertBoyer的推动下产生的。这个项目的目标，暂时被命名为QED项目或QED项目，在QED宣言中得到了概述，该文件于1994年首次发表，并得到了一些研究人员的支持。明确的作者身份被刻意避免了。一个专门的邮件列表被创建，并且举行了两次关于QED的科学会议，xxx次是1994年在阿贡国家实验室，第二次是1995年在华沙由Mizar小组组织。该项目似乎在1996年就已经解散了，除了讨论和计划之外，从未产生过更多的成果。在2007年的一篇论文中，FreekWiedijk指出了该项目失败的两个原因。按重要性排序。很少有人从事数学形式化的研究。

完全机械化的数学没有令人信服的应用。形式化的数学还不像真正的、传统的数学。这部分是由于数学符号的复杂性，部分是由于现有的定理证明器和证明助手的局限性；本文发现主要的竞争者Mizar、HOL和Coq在表达数学的能力方面有严重的缺陷。尽管如此，QED式的项目经常被提出来。Mizar数学图书馆将本科数学的很大一部分形式化，在2007年被认为是xxx的此类图书馆。类似的项目包括Metamath证明数据库和用Lean编写的mathlib库。2014年，作为维也纳逻辑学之夏的一部分，举办了”QED宣言二十年”的研讨会。