ReasLab 是面向教育、科研与复杂决策场景的一站式智能数学推理引擎，致力于让数学和应用触手可及，突破手工作业传统模式，构建从专家直觉驱动走向大众化、可计算、可验证的智能化基础设施。针对数学建模、算法设计与定理证明等关键环节长期相互割裂、深度依赖人工经验的问题，ReasLab 以大语言模型为基座，采用多智能体架构，融合数学模型库、算法库与定理知识库，将模型构建、算法设计、计算求解、自然语言和形式化证明及Markdown/LaTeX 报告生成等能力纳入统一环境，实现数学对象在不同表示层次与任务环节之间的贯通协同。依托云计算，用户无需安装即可在线使用。ReasLab 已为近千位用户提供形式化、优化建模、数学建模竞赛和科学写作等支持，为北京大学、新加坡国立大学等数十所高校提供形式化教学与科研工作空间，正服务华为、歌尔等企业实际需求，智能体 M2F 已形式化陶哲轩Analysis II、Rockafellar 的 Convex Analysis 等书籍，累计生成 Lean 代码30余万行，为数学研究与复杂决策提供可持续演进的基础支撑。ReasLab的研发得到了国家重点研发计划“大模型辅助运筹优化决策建模与计算”和国家重点研发计划“面向智能制造的约束规划算法与软件”资助与支持。
ReasLab用户交互示意图
致谢：
l 北京大学北京国际数学研究中心
l 大湾区大学/大湾区高等研究院
l 国家重点研发计划
l 国家自然科学基金
