vjb/LeanLLM：面向 Lean 4 的 LLM 证明循环与量子纠错码工具链开源项目

GitHub 上的开源项目 vjb/LeanLLM 结合三部分内容：一个 LLM 写 Lean 4 证明、编译器检错、错误回传重试的证明循环；Lagrange 定理的两种形式化；以及用于双变量 bicycle 量子纠错码的 Python 工具链。项目可为 IBM [[72,12,6]] 码构建 syndrome 电路并转译到 10×12 网格的 Nighthawk 模型，在 Qiskit Aer 噪声模型下仿真运行，还通过 MCP server 暴露 Lean 与 QEC 工具。作者强调这是可行性流水线，尚未在真实 IBM 硬件上运行，码距仅穷举到 weight 4。