haskell - 是否可以随机生成任意难以证明的定理？

Question

如果我正确理解 Curry-Howard 的同构，那么每个依赖类型都对应一个定理，实现它的程序就是一个证明。这意味着任何数学问题，例如，a^n + b^n = c^n都可以以某种方式表示为一种类型。

现在，假设我想设计一个生成随机类型（定理）的游戏，并且游戏必须尝试实现这些类型（定理）的程序（证明）。是否有可能控制这些定理的难度？即，简单模式会产生微不足道的定理，而困难模式会产生更难的定理。

Answer 1

单向函数是可以在多项式时间内计算的函数，但它没有可以在多项式时间内计算的右逆。如果f是一个单向函数，那么您可以选择一个x大小由难度设置决定的参数，计算y = f x并要求用户建设性地证明，即y在 的图像中f。

这不是很简单。没有人知道是否有单向函数。大多数人都相信有，但证明如果是真的，至少和证明一样难P /= NP。然而，有一丝光亮！人们已经设法构建了具有奇怪属性的函数，如果有的话功能是单向的，那么这些必须是。所以你可以选择这样一个函数，并且非常有信心你会提供足够困难的问题。不幸的是，我相信所有已知的通用单向函数都非常讨厌。因此，您可能会发现很难对其进行编码，并且您的用户可能会发现即使是最简单的证明也太难了。因此，从实际的角度来看，您最好选择像加密哈希函数这样的东西，它不太可能是真正的单向函数，但人类肯定很难破解。

Answer 2

Answer 3

这属于证明复杂性下限的有趣且困难的领域。首先，这在很大程度上取决于您使用的逻辑系统的强度，以及它允许​​的证明。一个命题在一个系统中很难证明，而在另一个系统中很容易证明。

下一个问题是，对于一个随机命题（在一个相当强的逻辑系统中），甚至不可能确定它是否可证明（例如，一阶逻辑中的可证明命题集只能递归枚举）。即使我们知道它是可证明的，确定它的证明复杂性也可能非常困难或无法确定（如果你找到了一个证明，这并不意味着它是最短的）。

直觉上它似乎类似于Kolmogorov 复杂性：对于一般字符串，我们无法判断产生它的最短程序是什么。

对于某些证明系统和特定类型的公式，存在已知的下限。哈肯在 1989 年证明：

对于足够大的n，PHP^n {n-1}_（鸽洞原理）的任何分辨率证明都需要长度 2^{\Omega(n)}。

这些幻灯片概述了该定理。所以你可以使用这样的模式生成命题，但这对于游戏来说可能不会很有趣。