Free Form Practice

How to use the blocks

Select a block to see the goal before that step. Fact menus list assumptions introduced by its enclosing blocks.

Select a block and open Built from to see the foundational blocks Lean turns it into: a proposition becomes constants applied to its parts, and a proof step becomes the partial proof it builds, with the goals it leaves shown as open. Hidden arguments, such as types Lean fills in, are collapsed until you show them.

The block menu has three tiers. Foundations holds the two sets everything else reduces to: the inference rules, and the kernel blocks for terms and declarations. Its blocks carry a ◆ mark. Built on the foundations holds shorter ways to write the same things, such as propositions, numbers and automation. Raw Lean takes Lean as text or as a syntax tree.

The Inference rules section lists the steps of a written proof: fix a variable, assume a hypothesis, claim a fact, use a fact, build the goal from its parts, take a fact apart, argue by induction or contradiction, rewrite, and restate by definition. fix and assume both emit Lean’s intro, but each is accepted only on its own kind of goal. A step that has no named rule can be written under Fill in any expression. Proof blocks read as a written proof; hover over one to see the Lean it emits, or open Generated Lean for the whole file. The names in code type below are those Lean names, which the block menu also searches.

Forward steps say what now holds and why: we have a fact, it suffices to show a claim, hence the goal, and a chain of equalities and inequalities. Each takes a reason from the Reasons section: the facts it follows from by logic, a fact applied to particular values, a theorem, linear arithmetic, algebra or computation. A reason lists the facts it uses, and Lean sees only those, so a side condition such as δ > 0 has to be stated before it can be used. Select a reason to see the goal it must justify.

A proof made only of inference rules, reasons and mathematical vocabulary is marked Written proof above the canvas. Two proof checkers, Lean and Rocq, check it side by side, and a step is accepted only when both accept it. Each reason means the same thing to both: “by the facts” is logic alone, “applied to” uses a “for all” fact for particular values, and linear arithmetic, algebra and computation are what they say. A Lean tactic, a kernel term, raw Lean or “clearly” makes it a Lean-only proof, which Lean alone checks.

Search the block palette for inference rules, core terms, Lean tactics, propositions, declarations, guided tools, goal suggestions, and saved blocks. Clicking a block places it near the selected step when a socket fits; otherwise it stays on the canvas. You can drag it, delete it, or use Undo.

A proof can be one constructed term: add exact expression, then combine names, application, functions, dependent function types, local values, universes, and annotations. A bound-variable block uses 0 for the nearest enclosing binder, 1 for the next, and so on; selecting it shows the available binders. Use refine expression with a proof hole ?_ to expose a goal for the following proof blocks. Lean checks the resulting term against the goal.

Every expression socket takes any term: a proposition such as P ∧ Q is a term, and it fits wherever a term does. An empty term socket is not an error. Lean reports the type it expects there, and the editor shows that on the block. Declarations form a list above the statement, and each can use the ones before it. To prove a declared theorem with inference rules, put a by block in its proof socket.

The statement editor has structured blocks for universes, axioms, definitions, total or partial recursive definitions, abbreviations, opaque constants, named theorems, mutual definitions, inductive types, structures, classes, and instances. Exact-name axioms, definitions, recursive and mutual definitions, theorems, and opaque constants can use numeric or unusual string name components. Axioms are unproved assumptions, so a document that adds one remains incomplete. Ordinary recursive definitions have parameter, termination measure, and decreasing proof sockets; exact-name recursion currently uses Lean’s automatic termination checking or partial mode. The term editor has match expressions and exact-name reference blocks. For an exact-name constant with no universe arguments attached, choose infer levels to let Lean fill them in or exactly zero for a constant with no universe parameters. Additional declaration forms and Lean extensions still need block grammars.

Use calc in a proof to connect relation steps. Put a proposition such as a = b and its proof term in each step; Lean checks that the relations compose.

Registered Lean syntax forms appear under Extended syntax. Forms can have typed, optional, or repeated sockets; show type from proof, lists, a scoped have, and an imported custom twice macro are available.

For a natural-number match, use Nat.zero in one constructor pattern and Nat.succ with a pattern-variable argument in another. Each branch has its own result term.

The two-branch constructor block creates two explicit branches; the general constructor block lets Lean expose however many goals its constructor creates. obtain unpacks a fact, and exact finishes a goal. For refine ⟨witness, ?_⟩, connect a term to the witness socket; Lean checks its type.

have contains a proposition, its proof, and a continuation. Its name is available only in the continuation. Practice lemma blocks create a socket for each premise.

In a custom conjecture, use term blocks to build types, properties, and theorem references. The natural-number blocks build sums, products, powers, divisibility, and coprimality claims. You can save a selected proof group under My blocks for reuse.

The Verbatim Lean section accepts proposition, term, declaration, and tactic syntax in a selected block. Use it when a structured block does not cover the Lean syntax you need. Local development checks these blocks; the deployed checker requires an isolated Lean worker before it can accept them.

Example: build ∀ x : Nat, Nat.Prime x with quantifier, proposition, constant, and application blocks. In the proof, intro x introduces the arbitrary number. Lean decides which facts are available at each step.

An error means this step did not prove the goal; it does not mean your conjecture is false.