autoform-bot

Autoform Bot 是一个用于将 LaTeX 数学文本自动形式化为 Lean 4 可验证证明的多智能体系统。它通过语句提取、多轮协作代理（调用 Claude/GPT/Gemini 等大模型）、Lean REPL 工具集成与数学库（Mathlib）协同，完成从自然语言数学命题到形式化定理及证明的端到端转换，并支持分布式执行（SLURM）与可视化追踪。适用于数学教材/论文的形式化迁移、教育场景中的证明辅助教学，以及形式化数学基础设施建设等需要高可信度自动证明生成的任务。