 gaojie
|
bb342fc492
|
docs(lean): 新增 HOWTO_PROOF.md — LeJEPA Lean4 证明过程完整指南
Sync to site1 / sync (push) Has been cancelled
内容涵盖：
- 为什么用 Lean4 做数学证明（vs 传统证明）
- 项目结构与文件依赖关系
- axiom vs theorem 核心概念
- 5 个证明文件逐行走读（Hermite/Uniqueness/Approx/Dirichlet/Planning）
- 关键 Mathlib 定理对照表
- 常用证明策略速查表（linarith/nlinarith/ring/field_simp 等）
- 如何添加新定理的完整步骤
- 调试技巧与常见错误解决
|
2026-06-05 17:37:50 +08:00 |
|