“把 Lean 想象成一门编程语言——就像你用 Python 写程序一样，你可以用 Lean 来写数学。（imagine Lean as a programming language the same way you use Python to write programs you can use Lean to write math）”— Leonardo de Moura
“AI 非常强大，但它会幻觉。Lean 确保你不必去检查 AI 找到的证明对不对。（AI is very powerful, but it hallucinates. Lean makes sure that you don't have to check if the proof AI found is correct or not.）”— Leonardo de Moura
“有一位用户告诉我：我已经知道证明了，我只是想把这个证明告诉系统——Lean 就是这样开始的。（one of the users told me 'I know the proof, I just want to tell this system the proof'. That's how Lean started.）”— Leonardo de Moura
“如果你的工作只是执行，它就可能被 AI 影响，因为 AI 执行得超快、又听从你的指令。（If your job is just to execute, it may be affected by AI... AI executes it super fast and follows your orders.）”— Leonardo de Moura
“如果你有一个想法，就跟 AI 聊——它会帮你把想法落地、帮你执行。（If you have an idea, talk to the AI to help you to execute on the idea.）”— Leonardo de Moura
术语 / 人物
Lean — 由 de Moura 创造的证明助手兼函数式编程语言，基于带归纳类型的构造演算，用于让计算机检查数学证明与程序的正确性，现广泛用于数学形式化与 AI 辅助定理证明。
Z3 — de Moura 早期创造的全自动 SMT（可满足性模理论）求解器，用于约束求解，可把软件 bug 查找、安全漏洞等可判定问题表述为数学问题自动求解。