Tab inserts an indent here. To move focus out of the editor, press Escape and then Tab.
The editor could not start in this browser. Everything else still works; your theory can be pasted once it loads, or submitted with curl.
Live output
As you type, the prover reads your source in the background. Output shows the goals at your cursor and the diagnostics (errors and warnings) for the whole document.
Each of these belongs to one revision of your source. After an edit it is replaced once the prover has read the new revision; until then it may still describe the text as it was.
The Pause button stops this background work; it then reads Resume, which starts it again for the current source and cursor. After a while without activity live updates pause on their own and the toolbar shows Paused · inactive; moving the cursor, editing or Resume starts them again. If the live prover cannot be reached the toolbar shows Unavailable · retrying; point at that status to see the reason.
Live goals and diagnostics are advisory. Check runs the prover over your whole source once, when you ask, and records its own result in Output; a proof found by Prove is verified afresh before it is reported. Only those results count.
Check reads your source; Prove fills in its one unfinished proof.