OpenGauss

Open Gauss 是一个面向 Lean 4 形式化证明项目的多智能体工作流编排工具，为数学定理证明、形式化建模等任务提供统一的 CLI 和项目管理界面。它集成了 lean4-skills 的核心能力（如 prove、draft、review、formalize 等），自动处理项目检测、后端会话管理、代理调度与状态恢复，并支持 Morph 在线托管与本地 tmux 部署两种模式。适用于数学研究者、形式化验证工程师及 Lean 社区开发者开展协作式定理证明、代码重构与自动化形式化任务。