是否有可能随机生成难以证明的定理？

Question

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

现在，假设我想设计一个生成随机类型(定理)的游戏，玩家必须尝试实现这些类型(定理)的程序(证明)。有可能控制这些定理的难度吗？也就是说，简单模式会产生琐碎的定理，而困难模式会产生更难的定理。

Answer 1

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

这并不是非常简单。没有人知道是否有任何单向函数。大多数人相信有，但要证明这一点，如果是真的，至少和证明P /= NP一样困难。然而，有一丝光芒！人们已经成功地构造了具有奇怪属性的函数，如果任何函数是单向的，那么这些函数就一定是单向的。所以你可以选择这样一个函数，并且非常有信心你会提供足够难的问题。不幸的是，我相信所有已知的通用单向函数都是相当糟糕的。因此，您可能会发现很难对它们进行编码，您的用户可能会发现即使是最简单的证明也太难了。因此，从实用的角度来看，您最好选择像加密散列函数这样的函数，它不太可能是真正的单向函数，但对于人类来说肯定很难破解。

Answer 2

如果只生成类型，那么它们中的大多数将与⊥同构。∀ n m -> n + m ≡ m + n是有意义的，但是∀ n m -> n + m ≡ n，∀ n m -> n + m ≡ suc m，∀ n m -> n + m ≡ 0，∀ n m xs -> n + m ≡ length xs和无数其他的没有意义。您可以尝试生成类型良好的术语，然后使用Djinn之类的工具检查生成的术语的类型是否不是一个简单得多的术语。然而，许多生成的术语要么过于简单，要么就是毫无意义的垃圾，即使有clever strategy也是如此。类型化设置包含的术语比非类型化的少，但只有一个变量的类型可以是A、A -> A、A -> B、B -> A、A -> ... -> E，并且所有这些类型变量都可以是自由的或全局量化的。此外，∀ A B -> A -> B -> B和∀ B A -> A -> B -> B本质上是相同的类型，所以您的相等不仅仅是αη，而是更复杂的东西。搜索空间太大了，我怀疑随机生成器能否产生真正重要的东西。

但也许某些特定形式的术语可能会很有趣。Agda 在评论中建议了参数化提供的定理:您可以简单地从标准库中提取Data.List.Base或Function或任何其他基本模块，并凭空生成许多定理。还可以查看A computational interpretation of parametricity的论文，该论文给出了从依赖类型设置中的类型导出定理的算法(不过，我不知道它与Theorems for free有什么关系，他们也没有给出数据类型的规则)。但我不确定大多数产生的定理不能通过直接的归纳来证明。然而，关于左折叠实例的函数的定理通常比关于右折叠实例的函数的定理更难--这可以是一个标准。

Answer 3

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

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

直观上看，它类似于Kolmogorov complexity：对于一般的字符串，我们不能说出生成它的最短的程序是什么。

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

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

These slides给出了这个定理的概述。因此，您可以使用这样的模式生成命题，但对于游戏来说，这可能不是很有趣。