Lea4——Lean 4 编程语言和定理证明器

LLPikaPika

Lean 是一种函数式编程语言，它使编写正确且易于维护的代码变得容易。
Lean 用作交互式定理证明器。Lean 编程主要涉及定义类型和函数。这使你的注意力可以集中在问题领域和操作其数据上，而不是编程的细节。
Lean 有许多特性，包括：类型推导、一等函数、强大的数据类型、模式匹配、类型类、可扩展的语法、卫生宏、依赖类型、元编程框架、多线程

Lean 是一门用于形式化证明的编程语言，它允许严格证明数学定理和验证软件代码的正确性

官网：https://lean-lang.org/
Github：https://github.com/leanprover/lean4
文档：https://lean-lang.org/documentation/
下载：https://lean-lang.org/download/

感兴趣的可以学习！！！

nyy

去tmd，编程语言还不够多吗？