THEOREM PROVING · OPEN TOOLING
Make an argument
answerable to proof.
A shared workbench for automated theorem proving, SMT solving, and interactive proof assistants. Choose a prover, enter a problem, and inspect the complete output.
AUTOMATED · HIGHER-ORDER LOGIC
Leo-III
Higher-order theorem proving with TPTP input.
Output
This tool is hosted by its project.
Open tool ↗Input here is sent to the third-party service. If embedding is blocked, open it directly in a new tab.
AResults are inspectable
Each run returns raw prover output and its reported status for independent review.
BTimeout is not a refutation
Resource limits constrain a run; they do not settle whether a claim is true or false.
CPremises remain visible
Formal validity is always relative to the axioms and encoding supplied.