概览

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

开始之前

• 创建账号：可通过邮箱或 GitHub 登录，约一分钟即可完成。详见 注册与登录指南。
• 创建或导入项目：可从零新建项目、从 GitHub 导入已有仓库，或通过分享链接加入他人项目。
• 浏览器要求：推荐使用最新版本的 Chrome、Edge 或 Safari，以获得完整功能体验。

核心应用场景

• 数学研究：开发形式化数学成果，发布经机器验证的可查验证明，提升研究可复现性。
• 教育教学：在协作式实验室中讲授定理证明、类型论与战术思维，支持师生共享实时工作空间。
• 软件验证：使用形式化方法对算法或软件组件进行精确规约与验证，减少安全关键代码中的缺陷。

功能快速索引

功能模块	详细说明
工作区布局与界面	工作区指南
Lean 4 编辑与 Infoview	Lean 工具链指南
实时协作	协作指南
AI 智能体配置	AI 供应商配置指南
LaTeX 编辑与 PDF 导出	LaTeX 指南
Markdown 实时预览	Markdown 指南
Git 版本控制	Git 集成指南