哥德尔的第一个不完全性定理指出，有些数学陈述既不能被证明，也不能被反驳。他的证明相当难理解——它涉及素数、因式分解，所有这些数字理论。哥德尔的证明必须很复杂，因为在1931年，计算机算法还没有真正被发明出来。
图灵机直到五年后的1936年才被发明。当证明停顿问题是不确定的——没有程序可以决定另一个项目是否会完成——哥德尔的工作给了他灵感。从历史上看，哥德尔·克利尔在图灵之前就开始了比赛。但在现代，对于那些已经理解“计算机程序”概念的人来说，从另一个角度理解这个理论要容易得多。先是图灵，然后是哥德尔。
这种精英的“元编程”技术使用程序wc来告诉您my_程序中有多少行代码。sh脚本。
你可以在程序上运行程序，在另一个程序上运行另一个程序。例如，如果你想知道在my_程序中计算代码行需要多长时间。上海：
现在想象一个名为behave_的脚本。sh.当你在另一个程序上运行它时，它会输出与该程序不同的东西。例如：
这可以输出任何东西，只要它与输出不同/我的课程。嘘/我的输入。txt。
对于任何剧本，悖论。嘘我的剧本。sh的行为与运行我的_脚本不同。嘘我的剧本。sh.那么当你跑步时会发生什么呢/矛盾的人嘘/矛盾的人嘘？这在逻辑上是不可能的。一定不可能写出不同的行为。嘘。
要表现出与其他脚本不同的行为似乎并非不可能。这种天真的做法会带来什么？
当你跑的时候/矛盾的人嘘/矛盾的人sh，脚本只是进入一个无限循环，什么也不输出。你可以查看我的工作——代码在GitHub上。它之所以很难与其他脚本有所不同，是因为当它进入一个长而安静的循环时，你无法判断这个循环是否真的是无限的。
如果我们有一个脚本暂停。如果能够判断程序是否会停止，我们可以用它来编写不同的行为。嘘。
所以写停顿肯定是不可能的。这就是停止问题的不可能性，图灵在1936年证明了这一点。
一旦你看到根本不可能的是写作，你的行为就会不同。嘘，你可以稍微概括一下停顿问题，这就开始有意义了。
有时，你可以证明一个程序进入了一个无限循环。智能编译器可以发现代码的某些区域是无法访问的。如果退出程序的所有部分都无法访问，那么程序必须进入无限循环。
你不需要理解所有的细节，在这里，你只需要知道有可能围绕这些证明构建一些工具。你可以用一个简单的例子来说明这些证据。校样文件格式，还有一个检查校样的保证脚本。所以当我们跑步时：
如果它返回YES，这意味着/我的课程。sh进入一个有限的循环。如果证明无效，验证程序将返回否。验证脚本本身永远不会进入无限循环。
我们需要的另一个工具是生成所有可能文件的方法。它可以非常慢，这很好。假设它通过将一个大整数转换成二进制表示来生成一个文件：
我们可以通过搜索目标脚本进入无限循环的证据来尝试表现出与目标脚本不同的行为。
#!/bin/bashi=0，为真；是的/生成_文件。sh$i>/可能的如果[[`./validate_-proof.sh./mably.proof$*`=="；YES"；]]则证明然后#目标进入无限循环。让'；s的行为不同退出0 fi i=$（（i+1））完成
如果有任何证据表明目标脚本进入了无限期，那么这个程序最终会找到它，并停止。如果没有证据，那么它将永远循环寻找证据。
如果每一个无限循环的程序都有一个无限循环的证明，那么我们只是写了不同的行为。我们知道这是不可能的。所以，无论我们使用什么样的证明系统，一定有一些程序永远不会终止，但没有证据表明它永远不会终止。必须有真实但无法证明的陈述，这是哥德尔在1931年证明的。
哥德尔的不完全性定理是数学哲学的基础。它表明了我们对真理的看法和我们对证据的看法之间的不匹配。它向我们表明，真理的理论概念和我们所知道的数学陈述的实际集合之间总是存在差异。
我希望这次展览对人们有所帮助。就我个人而言，我认为我们应该把哥德尔最初基于数论的证明作为历史事实放在一边，就像我们不再使用艾萨克·牛顿最初的微积分符号一样。我们应该承认，数学证明和计算机算法的概念是相互交织在一起的，首先要教停止的问题，其次要教数学证明的不完整性。