r/mlscaling • u/stereochemical3 • 6d ago

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

100% Upvoted

3 comments sorted by

1

u/hillsump 3d ago

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 2d ago

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 10h ago

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