Georges Gonthier

:35。1989年，最终的定稿以单行本的形式出版，超过400页。 对于机器证明的可靠性问题，2004年9月，数学家乔治·龚提尔（英语：Georges Gonthier）使用证明验证程序Coq来对当时交由计算机运算的算法程序进行形式上的可靠性验证。证明验证程序是一个由法国开发的软件，能够从逻辑上验证一