开源自动形式化代理 OpenGauss 发布，性能优于现有方案。

今天，在 @DARPA expMath 启动会上，我们推出了 𝗢𝗽𝗲𝗻𝗚𝗮𝘂𝘀𝘀，一个开源且最先进的自动形式化代理工具，供开发者和从业者在前沿加速进展。它比现成的替代方案更强大、更快、更经济高效。在 FormalQualBench 上，使用4小时超时运行，它击败了 @HarmonicMath 的 Aristotle 代理（无时间限制）。OpenGauss 用户可以按需与之交互，轻松管理多个并行子代理，并且可以扩展/修改/检查 OpenGauss，因为它是宽松开源的。OpenGauss 是与领先的开源 AI 工具（用于 Lean）的维护者紧密合作开发的。阅读报告并尝试：