GPT 周末补完 Erdos 形式化证明，数量翻倍

数学家 Boris Alexeev 为论证“自动形式化已经到来”，在周末让 GPT 为已形式化陈述、已有解答的 Erdos 问题直接补上 Lean 证明中的 sorry，成功使形式化证明数量翻倍，引发数学圈欢呼。这一做法通过命题预先形式化避免了语义对齐问题，突破了数学形式化中的瓶颈，被视为自动形式化进程的重要标志。

2026-08-19 ~ 2026-08-20 · 2 条相关