| ▲ | henryrobbins00 a day ago | |
I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms. To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback! I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others. [1] https://github.com/henryrobbins/open-atp | ||