我無法相信人類居然手動編寫 Lean 代碼。而且在 LLMs 出現之前，這些東西就已經在 Lean 中被正式化了。在 Lean 中正式化任何東西的感覺就像用土豆削皮器削掉自己的皮膚一樣令人愉悅，並且像看油漆乾燥一樣有趣。

別跟我說什麼「遊戲的樂趣」或「這麼互動」之類的。遊戲到處都是，就像到處都有ra*e一樣，我知道兩者之間的區別。

@notmoeezm "我根本不在乎機器是否驗證證明" 來源：一位為了好玩而調整證明空間搜尋算法的人，使用 Lean😞