Quickstart

Start a run

Open New Run, choose a launch mode, paste or upload statement.tex, then launch.

For most runs, keep the stable prover version selected and leave Generate paper on.

Write a good prompt

Define the problem precisely: include assumptions, notation, target statement, and any known constraints.

Fizzy Prover works best at filling in proof details, checking subclaims, and organizing a proof, not at discovering a solution from a vague problem statement.

If you already have a proof outline, include it. Even a rough outline can make the run much more efficient.

AI can make mistakes. Treat every generated proof as a draft and carefully check correctness yourself.

Watch progress

The run page shows status, elapsed time, config, versions, token usage, logs, and downloads.

Use Inspect to browse agent files when you need to read intermediate proof attempts.

Continue a run

Use Resume Run to continue from the existing run directory.

Use Restart Prover to restart from the current statement.tex.

Turn Generate paper off when you only want to run the prover and skip paper generation.

Download results

Use Downloads for statement.tex, root output, paper.pdf, paper.zip, and agents tex.zip.

agents tex.zip contains all agents/**/*.tex lifecycle files.