Albert Jiang (May 26 2022 at 10:01): Albert Jiang (May 26 2022 at 10:01):We have a preprint for our paper Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers: https://arxiv.org/abs/2205.10893!
We increased the proportion of solvable problems in the Archive of Formal Proofs for a language model from 39% to 57%, with the help of Sledgehammer. We also have a head-to-head comparison with OpenAI's IMO solver in Lean and slightly increased the success rate from 29.6% to 29.9%.
Last updated: Apr 26 2024 at 20:16 UTC