延续希尔伯特23个问题： 第24问题 是否存在一个通用算法，对于任意在形式算术（或任何足够强的形式系统）中可表达的真命题 ，都能在有限步内输出该命题的一个形式证明，并且所输出证明的长度（按符号数或步骤数度量）不超过该命题最短可能证明长度的某个可计算函数？ 换言之，能否有效逼近最优证明长度？若这样的通用算法不存在，请刻画那些允许“近似最优证明”的命题类，并研究最短证明长度作为命题的函数是否具有不可计算的复杂性。