嘿，这个问题刚好触碰到自动定理证明领域里一个挺有意思的方向！先理下背景：我们完全可以写一个程序，从ZFC（或者其他任意公理系统）的公理出发，遍历所有可行的推理规则，生成这个系统里能构造出来的所有证明——这类证明的总数是可数的。

要是我们有一台能解决停机问题的图灵机，用这种方法就能轻松判定任何数学问题的可证性，但可惜现实里压根不存在这种机器。不过我的疑问是：
有没有人真的开发过这类程序，专门遍历所有推理规则，目标是找出比如数学界20个最核心问题的证明？虽然没有停机机的话，这个过程可能永远跑不完，但说不定走着走着就碰巧撞上某个问题的证明了呢？

备注：内容来源于stack exchange，提问作者ThePhilosopher