Wiki. Lean [Lean]SimplicialCat 观念 Lean, 此处特指 Lean 4 (包含 Mathlib), 是一种基于类型论的, 用于做形式化数学的编程语言. 相关话题 AI 与形式化数学