Checks and proofs

Synthetic keeps track of what is proved in a Document, and of how far each result can be relied on. Lean judges each statement and each proof. Synthetic records what Lean was asked, what it answered, and whether that answer still holds for the Document as it is now.

It keeps these apart:

A reading is what a formula means, chosen by you where its notation reads more than one way.
A check of the statement asks Lean to state the reading, and shows you what Lean took it to say.
Your confirmation records that what Lean checked is what you meant.
A proof is a proof in Lean, written under the formula, of the reading you confirmed.
A check of the proof asks Lean whether the proof proves that reading, and says what the proof rests on.

A formula is proved only at the end of that chain. Confirming a statement says what it means; it doesn’t prove it.

From a formula to a proved result

In a Document, write (n : ℕ) → n = n. Type ℕ as \N and → as \to.
Press ⌘↵ (Ctrl+↵ off a Mac) to check it with Lean. The panel says “Lean 4 checked this statement, in Lean’s library”, and shows what Lean checked beside your formula.
Compare them. Where they agree, press They agree, and the panel says “You confirmed it matches what Lean checked”.
The formula now offers Prove. Press it, and Synthetic adds a proof under the formula: a Lean module that states your reading as the theorem t, with its proof left as sorry.
Replace sorry with fun n => rfl, and press Check proof. The proof’s line says “Lean accepted the proof, and the workspace accepts what it rests on”, and under it, “It rests on nothing beyond Lean’s kernel”. The reading is proved.

What a check of the statement can come to

Choosing a reading of a whole formula asks Lean to check it, where Synthetic can write the reading in Lean faithfully. The panel under the formula says what came of it:

“Lean 4 checked this statement, in Lean’s library”: the panel shows what Lean checked beside your formula. Where they agree, press They agree to confirm it. They differ moves on to the formula’s next reading, as Tab does. It doesn’t record a disagreement, and it doesn’t say Lean is wrong.
“Lean can’t state this reading”: Synthetic can’t write the reading in Lean faithfully, so it doesn’t send it, and the panel says why. The notation reference says which readings can be sent.
“Check failed: Lean couldn’t elaborate it”: Lean couldn’t make sense of the statement as sent, and its messages follow.
“Lean didn’t check the statement: it left obligations”: it doesn’t count as checked until they’re settled.
“Lean couldn’t check it this time”: Lean gave no answer. It may answer if you check again.

Confirming says what a statement means. It doesn’t prove it: Lean checks the statement with its proof left out, so a statement that Lean checked and you confirmed may still be false.

What a proof’s check can come to

The proof’s line says what came of its latest check:

“Lean accepted the proof, and the workspace accepts what it rests on”: the reading is proved here.
“Lean accepted the proof, but it isn’t accepted without review”, or “… but the workspace doesn’t accept what it rests on”: Lean found no error, but the proof rests on something your workspace doesn’t accept as it stands. See what a proof rests on.
“Lean rejected the proof”: Lean found an error in it, and its messages follow. This proof failed; that doesn’t make the statement false.
“The proof’s theorem states something other than the reading”: the module proves something, but not your reading. The line shows what Lean has where the reading differs, so a theorem about n = n + 0 never counts as a proof of n = n.
“Lean stopped at a limit before it decided” or “Lean left obligations”: Lean didn’t decide, so the proof doesn’t count.
“Lean couldn’t check the proof this time”: Lean gave no answer. Checking again may get one.

What a proof rests on

An accepted proof still rests on things Lean doesn’t prove: its foundations, and anything else the proof uses without proving it. The line under an accepted proof lists each one, such as:

“It rests on nothing beyond Lean’s kernel”;
“The proof uses propext, one of Lean’s foundations”;
“The proof is classical: it uses the axiom of choice (Classical.choice)”;
“The proof uses sorry”: the proof is unfinished, so it proves nothing, though Lean accepts a module that uses sorry;
“The proof rests on the axiom …”: an axiom the Document declares;
“The proof trusts a native computation (…)”: a computation run as compiled code rather than checked by Lean’s kernel.

Where the statement itself needs something, such as the axiom of choice, every proof of it does too, and the line says so of the statement: “The statement itself is classical”.

Your workspace’s trust policy decides which of these it accepts. By default, it accepts Lean’s three foundations: propext, Quot.sound and the axiom of choice. Anything else, such as sorry, a native computation or an axiom the Document declares, isn’t accepted without review, and there is no way to review one yet.

When a result stops counting

A result holds for one formula, one proof and one reading, as they were when Lean checked them.

You change the formula, the proof or its reading. The proof’s line says, for example, “Out of date: the formula changed since the proof was checked”. Check it again. Where Synthetic finds that a check no longer applies to the Document as it is, the line starts “No longer applies”.
You check the same proof again. The later check replaces the earlier one, which says “A later check of this proof replaced this one”.
Synthetic changes how it works with Lean. Synthetic sometimes changes how it checks with Lean, or how it writes readings for Lean, keeping the same release of Lean. It then checks each workspace’s confirmed readings and their proofs again the new way, and moves the workspace to it once those checks have finished. A proof that still checks keeps its result, and one that doesn’t shows what Lean says now. If Lean now takes a confirmed statement to say something else, your confirmation of it no longer stands, and you can compare and confirm it again. Synthetic can’t yet move a workspace to a newer release of Lean itself.

Why you can rely on what it says

What you confirm is what Lean checked. The statement shown beside your formula is read back from what Lean’s kernel checked, not from Lean’s printed text, which can look right while meaning something else.
A proof proves your reading, or it doesn’t count. A proof whose theorem states anything else, however close, is reported as that, never as a proof of your reading.
What a proof rests on comes from what the kernel checked, so a proof can’t hide an axiom or a sorry behind its text.
Lean runs each proof in a sandbox with no network access, as a proof’s module can run code while Lean reads it.

Who sees what

Your checks are yours. Others who can read the Document don’t see the checks you ask for, or what came of them.
So is your confirmation.
A Document commits to one reading of each formula: the reading its editors stand by. When an editor confirms a reading, it becomes the one committed. Where another editor committed a different reading, the panel asks whether to keep theirs or use yours. Someone who can only read the Document can confirm only the reading an editor committed.

Proofs from the agent

The agent can work on a proof in Lean, and where you can edit the Document, it can propose one. A proposed proof shows in place, with what its own check came to. That Lean accepted the agent’s steps doesn’t prove your reading. When you accept a proposal whose proof its own check found sound, the Document page checks the proof again in the Document. Otherwise, check it there yourself: press Check proof.

Limits

A workspace checks with Lean’s own library, without Mathlib, and no page offers Mathlib yet. So a proof can use what Lean itself provides, and statements that need Mathlib, such as ones about the real numbers, can’t be checked yet.
You can have one check running at a time. Another is refused until it ends, and Stop ends a running check.
Not every reading can be stated in Lean faithfully, and a check speaks only for the statement Lean was sent.