autoform-bot

Autoform Bot 是一个用于将LaTeX数学内容转换为经验证的Lean 4证明的多代理系统。其核心功能包括从LaTeX文档中提取数学语句，并通过与Mathlib集成，利用多种语言模型（如Claude、GPT和Gemini）来生成和验证这些证明。该工具支持分布式计算环境下的高效运行，提供了一个可视化仪表盘以监控处理流程及结果。适用于需要自动化生成或验证形式化数学证明的研究场景，尤其是在数学、计算机科学领域内进行大规模文献分析时能够显著提高工作效率。