我无法相信人类居然手动编写 Lean 代码。而且在 LLMs 之前，这些东西就已经在 Lean 中被正式化了。在 Lean 中正式化任何东西的感觉就像用土豆削皮器削掉自己的皮肤一样令人愉悦，和看油漆干一样有趣。

别跟我说什么“游戏的乐趣” / “它是如此互动”之类的。游戏到处都是，就像到处都有ra*e一样，我知道两者之间的区别。

@notmoeezm "我根本不在乎机器是否验证证明" 来源：一个为了乐趣而调试证明空间搜索算法的人，使用 Lean😞