Lean in the Workspace

With Lean installed, a theorem and its proof are checked in the same document as the computations, and a computation can sit between two proof steps. Lean is chosen from the engine control beside the four CAS, or for one line by right-clicking it: Execute in Lean. The CAS computes, Lean checks.

Every picture below is a screenshot of a Workspace document, taken after running it with Lean.

Learning Lean in the Workspace

Help > Tutorials > Lean 101 starts from proofs on paper. Each of its thirteen sections takes one familiar move (assume, split a claim, replace equals, cite a known theorem, exhibit a witness, induct) and shows it in Lean, on number theory: remainders, divisibility, gcd, Pell equations, the Euclidean algorithm, finite sums. The last section has a CAS exploring and Lean certifying. Every section ends with an exercise whose solution is live: it runs, and it can be edited and checked again.

Read Lean 101 here, with the results of its own run →

A computation between two proof steps

A proof that every odd number is a leg of a Pythagorean triple (3, 4, 5; 5, 12, 13; 7, 24, 25; …), with SymPy finding the other two sides. Lean needs the two sides to check; SymPy solves for them, as formulas in k.

The theorem odd_leg, its Proof checked verdict, the existential goal, a SymPy solve line giving b = 2k^2 + 2k and c = 2k^2 + 2k + 1, then use with those two sides, the goal it leaves, and ring ending in No goals — In the picture, at the top, the theorem as written; below it, the same proof step by step, each step followed by the goal it leaves (⊢ …), with the SymPy line between two steps. The SymPy line was put between the proof steps with a right-click on the theorem’s header, **Insert CAS computation here**.
With c − b = 1, the equation (2k + 1)² = c² − b² = (c − b)(c + b) leaves c + b = (2k + 1)²; SymPy’s `solve` gives b = 2k² + 2k and c = 2k² + 2k + 1. `use` supplies them, and `ring` verifies the identity for every integer k.

From a CAS result to a Lean theorem

The other direction: a CAS result becomes a Lean theorem. Sometimes a CAS answer holds only under a condition it does not state; SymPy and other CAS cancel (x² − 1)/(x − 1) to x + 1. With a right-click on its line, Use as Lean candidate, the Workspace writes the theorem for that answer; the theorem carries the hypothesis x − 1 ≠ 0, and Lean checks it.

The SymPy line cancel((x^2-1)/(x-1)) returning x + 1, the candidate theorem with hypothesis h1: x - 1 not equal to 0, its Proof checked verdict, then field_simp and ring ending in No goals — Above the theorem, the note of where it came from, with its assumptions, x ∈ ℝ and x − 1 ≠ 0. The Workspace wrote the proof, `field_simp` then `ring`; `field_simp` uses x − 1 ≠ 0 to clear the denominator, and Enter had Lean check it.
So, the cancellation holds for every real x except 1.

The goals under each step

Enter checks a theorem and shows its proof as successive steps, as written, each with the goals that remain after it; some nested tactics are grouped into one step. A step can be edited in place: the edit changes the theorem, marks the proof Outdated, and Enter checks it again. After a hand edit of the theorem itself, the steps are read-only until it is checked again.

The statements and goals are typeset as mathematics, the tactics as words. A click on an input opens its Lean source, as typed, with the cursor where the click landed; Enter checks it and shows it typeset again. The symbols are typed as in VS Code: \N and a space give ℕ, \forall ∀, or they come from the Math palette.

From Lean 101, section 1: a one-step proof, Fermat’s little theorem at p = 101, 2¹⁰⁰ ≡ 1 (mod 101).

The theorem fermat_two_mod_101, 2 to the 100 mod 101 equals 1, its Proof checked verdict, the goal under the header, then rfl and No goals — `rfl` settles it by computation: Lean evaluates 2¹⁰⁰, a 31-digit number, and its remainder on division by 101.

From Lean 101, section 2: a proof in five steps, for integers a, b, c, if a divides b, then a divides bc.

The theorem divides_product, its Proof checked verdict, then intro, obtain, use, rw and ring, each followed by the hypotheses and the goal it leaves, ending in No goals — In Lean, a ∣ b means b = a·k for some integer k: `obtain` names that k, and `use k*c` supplies the factor the conclusion needs, b·c = a·(k·c).

What “Proof checked” means

“Proof checked” appears for a complete proof, checked by Lean, with no sorry anywhere it depends on. A person, a tactic, a CAS or an AI may suggest the proof; Lean’s kernel accepts the resulting proof, or it does not. An unfinished proof shows its remaining goals; a failure shows Lean’s own message on its line. A reopened document shows “Saved check” until Enter checks it on this computer. .lean files open as Lean documents, and a document exports to a .lean file with each CAS line as a comment.

Lean is not bundled: Help > How to > Setting up Lean explains how to install it with its Mathlib library, which takes several gigabytes of disk; with Mathlib loaded, a Lean document also takes several gigabytes of memory.

← The Workspace

VS Code and Workspace displays of the same proof

The same one-step proof, 2¹⁰⁰ mod 101 = 1, in VS Code and in the Workspace.

VS Code shows the state at the cursor; the Workspace shows every state, in order. “Goals accomplished!” in InfoView is Lean’s own message; “Proof checked” is the Workspace’s verdict from the same evidence; it also reports which axioms the proof uses.

VS Code with the cursor before rfl, and beside it InfoView's tactic state: one goal, 2 to the 100 mod 101 equals 1 — The state at the cursor, before `rfl`: one goal, `2^100 % 101 = 1`.

The Workspace: the theorem, its Proof checked verdict, the goal 2 to the 100 mod 101 equals 1 under the generated header, then rfl and No goals — Every state, in order: the goal 2¹⁰⁰ mod 101 = 1, then `rfl`, then no goals.

In VS Code, moving the cursor through the proof updates InfoView to the state at that point. In the Workspace every state is on the page at once; a click on an input opens its source for editing (symbols from the palette or \abbreviations), an edited proof is marked Outdated, and Enter checks it again.