來自 Alexander Doria（@Dorialexander）的推文串

由於 Lean 已成為自動形式化的參考語言，因此值得記住的是，內部錯誤是如何演變成 DS-Prover-v2 的獎勵破解的。

我不確定目前的格局是否已經定型，或許也不該定型。許多其他語言用於特定領域（通常用於編寫基於規則的約束），但用於合成的基準測試/資料集/配方卻幾乎不存在。