diff --git a/docker/README.md b/docker/README.md
new file mode 100644
index 0000000..234b265
--- /dev/null
+++ b/docker/README.md
@@ -0,0 +1,45 @@
+[Dockerfile](/Users/zzyang/ProjectResearch/lean-bench/docker/Dockerfile)
+构建完整运行镜像：
+- 基于 Ubuntu 24.04。
+- 安装 Python、Git、curl、SQLite 等。
+- 安装 elan。
+- 解析 Mathlib 和 Lean 兼容版本。
+- 运行 lake update。
+- 下载 Mathlib 预编译缓存。
+- 用真实 Lean 编译 smoke 文件。
+- 安装 lean-bench Python 包。
+- 配置数据库、LLM 和 Lean 环境变量。
+- 挂载 /books 与 /data。
+镜像很重，Mathlib 缓存和编译对内存、磁盘要求较高。
+
+[docker-compose.yml](/Users/zzyang/ProjectResearch/lean-bench/docker/docker-compose.yml)
+本地 Docker Compose 配置：
+- 构建或拉取 lean-bench 镜像。
+- 注入 DashScope API Key 和模型设置。
+- 把本地 books/ 映射到 /books。
+- 把本地 data/ 映射到 /data。
+- 默认运行 doctor。
+
+[entrypoint.sh](/Users/zzyang/ProjectResearch/lean-bench/docker/entrypoint.sh)
+容器入口：
+- 创建数据库父目录。
+- 设置运行环境。
+- 把用户传入参数交给 lean-bench。
+- 允许镜像直接执行 ingest、search 等子命令。
+
+[resolve-mathlib.sh](/Users/zzyang/ProjectResearch/lean-bench/docker/resolve-mathlib.sh)
+构建阶段解析 Lean/Mathlib 兼容性：
+- 接受显式 Mathlib revision 或 auto。
+- 查找合适的 Mathlib revision。
+- 根据 Mathlib 对应配置确定 Lean toolchain。
+- 更新 Lean 工程配置。
+它解决“Lean 版本和 Mathlib revision 不兼容”的常见构建问题，但动态解析降低了可复现性。
+
+[smoke.py](/Users/zzyang/ProjectResearch/lean-bench/docker/smoke.py)
+Docker 中的端到端 smoke test：
+- 使用脚本化 LLM 回复。
+- 走完整 ingest 流程。
+- 调用真实 Lean，而不是 fake checker。
+- 写入临时 SQLite 数据库。
+- 检查生成条目确实被 Lean 验证并可查询。
+这曾经由 Docker CI 调用；工作流删除后，当前没有自动执行者。
\ No newline at end of file