bash pip install lean-dojo

按照官方指引安装 Lean 4 对应版本

### 5.2 加载数学库与定理
在 Lean 中新建文件 `mylearn.lean`，写入一个简单定理：
```lean
import Mathlib
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    simp
  | succ a ih =>
    simp [ih, Nat.add_comm, Nat.succ_add, Nat.add_succ]

5.3 通过 Python 与环境交互模拟证明

使用 LeanDojo 的 TacticState 读取目标：

from lean_dojo import LeanDojo, TacticState, Observation
dojo = LeanDojo(lean_file="path/mylearn.lean")
# 获取初始状态
init_state = dojo.run_tac("theorem add_comm (a b : Nat) ...")
print(init_state.pp_goal)
# 执行一个 tactic，返回新状态与反馈
next_state, message = dojo.run_tac("induction a", state=init_state)
print(next_state.pp_goal)

5.4 搭建一个简单的强化学习循环

伪代码：

model = load_LLM()
for episode in range(max_episodes):
    state = env.reset(theorem)
    done = False
    while not done:
        action_probs = model(state)
        action = sample(action_probs)
        next_state, reward, done, info = env.step(action)
        # 存储 (state, action, reward, next_state, done)
        store_in_buffer(...)
        if done and reward == +1:
            # 成功，记录成功路径
            add_to_success_dataset()
    # 每收集足够数据后更新策略
    policy_loss = compute_PPO_loss()
    update_model(policy_loss)