From d2bbbacfa842e0b34aee27537ec6a12a65be1e4f Mon Sep 17 00:00:00 2001
From: Zayden-Jung <zayden.jung@entroia.com>
Date: Tue, 22 Sep 2026 16:49:52 +0000
Subject: [PATCH] Add lean/README.md

---
 lean/README.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 lean/README.md

diff --git a/lean/README.md b/lean/README.md
new file mode 100644
index 0000000..981acd2
--- /dev/null
+++ b/lean/README.md
@@ -0,0 +1,16 @@
+[lean-toolchain](/Users/zzyang/ProjectResearch/lean-bench/lean/lean-toolchain)
+指定 Lean 工具链版本，供 elan 和 Lake 使用。
+
+[lakefile.toml](/Users/zzyang/ProjectResearch/lean-bench/lean/lakefile.toml)
+Lean Lake 工程配置：
+- 定义项目。
+- 声明 Mathlib 依赖。
+- 让 lake env lean 能在正确环境中加载 Mathlib。
+Mathlib 精确 revision 主要在 Docker 构建时解析，而不是完整锁定在仓库中。
+
+[LeanBench.lean](/Users/zzyang/ProjectResearch/lean-bench/lean/LeanBench.lean)
+Docker 构建时使用的 Lean smoke 文件：
+- 导入 Mathlib。
+- 放置少量声明。
+- 验证 Mathlib olean、Lean 工具链和 lake env lean 能实际工作。
+它不是项目运行时库，主要是环境健康检查。
\ No newline at end of file