今天，在 @DARPA expMath 啟動會上，我們推出了 𝗢𝗽𝗲𝗻𝗚𝗮𝘂𝘀𝘀，這是一個開源且最先進的自動形式化代理工具，旨在幫助開發者和從業者加速前沿進展。 它比現成的替代品更強大、更快速且更具成本效益。在 FormalQualBench 上，運行時間限制為 4 小時，它在沒有時間限制的情況下擊敗了 @HarmonicMath 的 Aristotle 代理。 OpenGauss 的用戶可以根據自己的需求進行互動，可以輕鬆管理多個並行工作的子代理，並且可以擴展/修改/檢查 OpenGauss，因為它是寬鬆的開源。OpenGauss 是與領先的開源 AI 工具 Lean 的維護者密切合作開發的。 閱讀報告並試用：