Patrick Hillmann|2026年05月28日 20:48
上周，OpenAI 展示了 AI 可以帮助发现新的数学。我们将他们的结果形式化为 Lean 4 中可由机器验证的证明。
这不仅仅是学术研究。这是将 AI 引入对准确性要求极高的关键系统的一步。
https://(logicalintelligence.com)/blog/aleph-prover-erdos-disproof-lean-4-formal-methods
+5分享至：
脉络
热门快讯
APP下载
X
Telegram
复制链接