Results are inspectable
Each run returns the prover's raw output and its reported status, so a claim can be reviewed independently rather than taken on trust.
Automated provers & proof assistants
Formal Reasoning Lab
Reason with precision, and inspect exactly what each tool returns.
Explore an argument with automated theorem provers and proof assistants. The premises, the raw output, and the reported status stay in full view — a claim can be examined, not just asserted.
6
Tools
4
Local runners
2
Online services
60s
Run limit
The workbench
Select a toolAutomated · Higher-order logic
Leo-III
Higher-order theorem proving with TPTP input.
Output
Hosted by its project.
Open tool
Input you enter here is sent to the third-party service. If embedding is blocked, open the tool directly in a new tab.
How to read a result
Terminology legend: sat, unsat, Theorem, inference steps, and more →
Timeout is not a refutation
Resource limits constrain a single run; they do not settle whether a proposition is true or false.
Premises remain visible
Formal validity is always relative to the axioms and encoding supplied. The input stays in view alongside the result.