Announcement in X [1].
"""
Today, at the
@DARPA
expMath kickoff, we launched , an open source and state of the art autoformalization agent harness for developers and practitioners to accelerate progress at the frontier.
It is stronger, faster, and more cost-efficient than off-the-shelf alternatives. On FormalQualBench, running with a 4-hour timeout, it beats
@HarmonicMath's Aristotle agent with no time limit.
Users of OpenGauss can interact with it as much or as little as they want, can easily manage many subagents working in parallel, and can extend / modify / introspect OpenGauss because it is permissively open-source. OpenGauss was developed in close collaboration with maintainers of leading open-source AI tooling for Lean.
"""
Announcement in X [1]. """ Today, at the @DARPA expMath kickoff, we launched , an open source and state of the art autoformalization agent harness for developers and practitioners to accelerate progress at the frontier.
It is stronger, faster, and more cost-efficient than off-the-shelf alternatives. On FormalQualBench, running with a 4-hour timeout, it beats @HarmonicMath's Aristotle agent with no time limit.
Users of OpenGauss can interact with it as much or as little as they want, can easily manage many subagents working in parallel, and can extend / modify / introspect OpenGauss because it is permissively open-source. OpenGauss was developed in close collaboration with maintainers of leading open-source AI tooling for Lean. """
[1] https://x.com/mathematics_inc/status/2034700606498083025