来自 Alexander Doria（@Dorialexander）的推文线程

由于 Lean 已成为自动形式化的参考语言，因此值得记住的是，内部错误是如何演变成 DS-Prover-v2 的奖励破解的。

我不确定目前的格局是否已经定型，或许也不应该定型。许多其他语言用于特定领域（通常用于编写基于规则的约束），但用于合成的基准测试/数据集/配方却几乎不存在。