今天，在 @DARPA expMath 启动会上，我们推出了 𝗢𝗽𝗲𝗻𝗚𝗮𝘂𝘀𝘀，一个开源的、最先进的自动形式化代理工具，旨在帮助开发者和从业者加速前沿进展。 它比现成的替代品更强大、更快速且更具成本效益。在 FormalQualBench 上，运行时间限制为 4 小时，它在没有时间限制的情况下击败了 @HarmonicMath 的亚里士多德代理。 OpenGauss 的用户可以根据自己的需求与其进行交互，可以轻松管理多个并行工作的子代理，并且可以扩展/修改/检查 OpenGauss，因为它是宽松的开源。OpenGauss 是与领先的开源 AI 工具 Lean 的维护者密切合作开发的。 阅读报告并试用：