有可能随机生成任意难以证明的定理吗？

Question

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

现在,假设我想设计一个生成随机类型(定理)的游戏,并且游戏必须尝试实现这些类型的程序(证明)(定理).是否有可能控制那些定理的难度？即,简单模式将产生平凡定理,而硬模式将产生更难的定理.

Answer 1

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

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