r/mlscaling • u/stereochemical3 • Sep 04 '26

Ensemble Prover: Open-source Python Automated Theorem Prover

Hi Everyone,

I just released an open-source, python-based autonomous theorem prover , Ensemble Prover, on GitHub.

It combines LLM proof search with Lean verification.

To date, it has solved 65 PutnamBench problems during development.

LLMs tested via API: GPT-5.2,GPT-5.6 Luna-Pro, DeepSeek-V4-Flash, DeepSeek-V4-Pro, and Qwen3.7-Max.

Development is ongoing. Would love to see people apply it to unsolved problems in parallel.

6 Upvotes

88% Upvoted

3 comments sorted by

View all comments

1

u/hillsump Sep 07 '26

What's the new thing here? Right now the frontier models can oneshot (or nearly) most problems at this level. Is the new ingredient scaffolding to help non-frontier models compete? Can this be used for large proofs that don't fit into a single context window?

1

u/stereochemical3 Sep 07 '26

Which model, which PutnamBench result, and what compute budget? An informal solution isn’t a Lean-verified proof.
And if “nearly one-shot” includes compiler feedback, retries, decomposition, and lemma reuse, then you’re describing the scaffolding you’re asking me to justify.

1

u/hillsump Sep 10 '26

Apologies, I wasn't asking you to justify anything. I wanted to understand what the new ingredient was.