Prover9 & Mace4
Enhanced for the next decade

Prover9 is a resolution and paramodulation-based theorem prover for first-order and equational logic, and Mace4 searches for finite counterexamples. Both were developed by William McCune at Argonne National Laboratory, and together proved instrumental in the solution of the Robbins Problem and numerous other open questions in algebra. Jeffrey P. Machado and Larry Lesyna have built upon the solid foundation that McCune left the world in 2009. It is their hope that Prover9 and Mace4 will continue to be used by students, educators, and researchers throughout the 21st century.

This site is the new home of the LADR-2026 project — a comprehensive modernization of McCune's codebase, faithful to his documented intentions. The TPTP input support in particular fulfills a goal he left written in the manual. His underlying algorithms are unchanged; we've repaired what was broken and extended what was limited.

LADR-2026 passes classical proof benchmarks through Ivy and GDV verification, including 1.00-rated problems in the TPTP library. The portfolio strategy selector — trained on 32 problem features — significantly reduces time-to-proof on hard problems.