Inria, Palaiseau , France.
Philos Trans A Math Phys Eng Sci. 2019 Mar 11;377(2140):20180038. doi: 10.1098/rsta.2018.0038.
In this short overview article, I will discuss the problem of proof identity and explain how it is related to Hilbert's 24th problem. I will also argue that not knowing when two proofs are 'the same' has embarrassing consequences not only for proof theory but also for certain areas of computer science where formal proofs play a fundamental role, in particular, the formal verification of software. Then I will formulate a set of four objectives that a satisfactory notion of proof identity should obey. And finally, I discuss Hughes' combinatorial proofs and argue that they can be seen as a first step towards a possible solution to the problem of proof identity. This article is part of the theme issue 'The notion of 'simple proof' - Hilbert's 24th problem'.
在这篇简短的综述文章中，我将讨论证明身份的问题，并解释它与希尔伯特第 24 个问题的关系。我还将论证，不知道两个证明何时“相同”，不仅对证明理论，而且对计算机科学的某些领域，包括形式证明起着根本作用的领域，如软件的正式验证，都会产生尴尬的后果。然后，我将制定一组四项目标，一个令人满意的证明身份概念应该遵守这些目标。最后，我讨论休斯的组合证明，并认为它们可以被看作是解决证明身份问题的可能的第一步。本文是主题为“简单证明的概念——希尔伯特第 24 个问题”的一部分。
