Wake up babe, new superintelligence company just dropped
And they show some impressive results.
The Math Inc. team is excited to introduce Gauss, a first-of-its-kind autoformalization agent for assisting human expert mathematicians at formal verification. Using Gauss, we have completed a challenge set by Fields Medallist Terence Tao and Alex Kontorovich in January 2024 to formalize the strong Prime Number Theorem (PNT) in Lean (GitHub).
Gauss took 3 weeks to do so, which seems way out of METR task length horizon prediction. Though I’m not sure if that’s fair comparison, both because we do not have baseline human time for this task, and because formalizing is a domain where it is very hard to get off track, the criterion of success is very crisp.
I think alignment researchers have to learn to use it (or any other powerful math prover assistant) in order to exploit every leverage we can get.
Wake up babe, new superintelligence company just dropped
And they show some impressive results.
Gauss took 3 weeks to do so, which seems way out of METR task length horizon prediction. Though I’m not sure if that’s fair comparison, both because we do not have baseline human time for this task, and because formalizing is a domain where it is very hard to get off track, the criterion of success is very crisp.
I think alignment researchers have to learn to use it (or any other powerful math prover assistant) in order to exploit every leverage we can get.