Lean
Lean是一种用于形式化和检验数学证明及程序性质的定理证明助手，同时也是一种编程语言。
3篇文章
最近提及 Lean是由Microsoft Research的Leonardo de Moura于2013年开始开发的开源定理证明助手和函数式编程语言。用户用形式语言编写数学命题与证明后，由计算机逐步检查证明。自2023年起，其开发由非营利组织Lean FRO主导。
Lean用于数学形式化和软件验证，社区维护的数学库mathlib被广泛使用。在人工智能领域，它也被用来对模型生成的证明进行机器检验。
本条目依据AIPOST的文章与广为人知的事实整理。如有错误，请通过更正请求告诉我们。
涉及该条目的文章
在5月27日的一起事件中，一个内部模型正在处理一项Lean任务。
OpenAI既公布了分析论文，也公布了在Lean中形式化的证明。