用途：面向 Lean 4 的形式化定理证明、数学验证、证明搜索与类型论推理，也可用于程序验证和基于 Mathlib 的形式化数学。不适用于数值计算（用 scipy/numpy）、符号代数或微积分（用 sympy）、统计分析（用 statsmodels）以及快速计算。
主要能力：提供定理结构（如 rfl、apply、intro、omega 等写法）与核心策略，包括 intro、apply、exact、rfl、simp、ring、omega、linarith、cases/rcases、induction、constructor、contradiction；可结合 Mathlib 使用 norm_num、positivity、polyrith、gcongr、field_simp 等。
使用方式：若未安装 lean，可用 elan 安装：curl https://elan.lean-lang.org/install.sh -sSf | sh，或 macOS 上 brew install elan-init，然后 elan default leanprover/lean4:stable。用 lake new my_project 创建项目，在 lakefile.lean 中配置 Mathlib 依赖，执行 lake update 与 lake build。可用 lean MyFile.lean 运行文件，用 #check、#eval、#print 探索；交互式证明建议在 VS Code 配合 lean4 扩展查看目标状态。
适用场景：形式化数学、定理证明、类型论探索、程序验证。
限制与建议：资料未提供收费、平台与效果信息。建议在 lakefile 中设置 autoImplicit 为 false 以捕获变量名拼写错误；开发中可用 sorry 占位，但最终需消除；多用 #check 检查类型；证明保持模块化；Mathlib 项目可运行 lake exe cache get 下载预构建 oleans 加速构建。