RecodeX 重构消息，Meta的FAIR研究组织与纽约大学（NYU）等机构的研究人员于10月25日发布论文《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》，提出AI定理证明系统h1。

在共同评估的5个埃尔德什问题上，h1单次运行成功率为82.5%，每个成功证明的平均API折算成本为121美元。同一问题集上，AlphaProof Nexus成功率为76%，每个成功证明成本为317美元；但纳入第六个问题后，h1的成功率下降至68.75%。研究团队还比较了h1与其他定理证明系统的性能与成本，并在多个基准上评估语言模型的证明能力。