Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [pdf]

Tested in the article:

miniF2F: https://github.com/openai/miniF2F

PutnamBench: https://github.com/trishullab/PutnamBench

..

FrontierMath: https://arxiv.org/abs/2411.04872v1

Has Sanjeev Arora pivoted to AI? Was he always interested in this? I thought he was more of a theoretician.

Maybe he’ll crack why DNNs work, whatever that means. To answer that question you have to formalize what it means for them to “work”. Good luck defining that in a reasonable way.

The majestic genius of Gödel was finding a way of exhibiting an unprovable truth.*

* yes, assuming consistency