Lean Copilot 在 NeurIPS MATH-AI 展示 LLM 原生嵌入 Lean：从 autonomous prover 转向 human-in-the-loop proof copilot

NeurIPS 2023 MATH-AI Workshop 上，Lean Copilot 展示把 LLM inference 直接集成进 Lean workflow：支持 tactic suggestion、proof search、premise selection，并允许用户使用本地或云端模型。与同期强调全自动 proving 的系统不同，Lean Copilot 明确把人类 insight 保留在交互回路中，定位为 proof engineering copilot；代码公开并可在 Lean 4 中使用。