Explicit runtime
Therefore runner checks target Lean 4.30.0. Lean Web uses its own displayed project and toolchain.
Interactive Lean
Write a declaration. Ask Lean to check it.
Start from any proof in the executable corpus, edit the Lean source, and inspect compiler diagnostics. Checks use Therefore's isolated runner when it is connected. Otherwise, you can explicitly load the code into the embedded community-run Lean Web service.
Lean 4.30.0100 runnable startersLean syntax highlighting
Main.lean
Isolated execution
User code belongs in a disposable worker with no application secrets or shared writable cache.
Precise status
Only a valid Therefore runner response becomes passed or failed. Embedded Lean Web diagnostics are never presented as Therefore verification.