ExaktAI

ExaktAI Workspace: Lean 101

A compact, live introduction to writing mathematics and checking proofs in the Workspace. This tutorial assumes mathematical familiarity but no Lean experience. Open a section, run its examples, then change something and observe the goals. The early sections introduce the language; the later ones build proofs and combine Lean with CAS exploration.

This tutorial runs on your own Lean installation, with Mathlib. Tools ▸ Check CAS and AIs shows whether Lean is ready on this computer; Help ▸ How to ▸ Setting up Lean describes the installation.

This is the tutorial as it ships with the Workspace (Help > Tutorials > Lean 101), with the results of its own run. To run an example, change it and check it again, open it in the Workspace. ← Lean in the Workspace

How to use this live tutorial

The document is Lean → Lean. Read and run its original inputs from top to bottom. Enter checks an input; Shift+Enter adds a line within it. Names introduced earlier are available later. Explanations are separate text regions. The results you see were produced when the tutorial was made; Enter checks an input again, on your own Lean installation.
A complete proof can occupy one multiline input. After checking, Workspace displays generated proof inputs and their goals. You can edit the original input or a generated proof input: an edit in a generated input changes the original at once, and the goals shown become outdated until you press Enter. After you edit the original itself, its generated inputs are read-only until the next check. The displayed goals belong to that checked step, not to wherever you move the cursor. Rechecking may process preceding source again.
The Workspace finds your Lake project with Mathlib by itself: Tools → Check CAS and AIs → Lean shows which project and toolchain it uses, reports Lean and Mathlib ready, and lets you choose another project. A document need not say import Mathlib: when a Lean document opens, the Workspace starts loading Mathlib in the background. Until it is loaded, an input is checked with Lean alone, at once; a result reached that way is marked “(core Lean)”. An input that needs Mathlib first shows Lean's answer without it, then is checked again with Mathlib as soon as it has loaded, which takes several seconds the first time in a session. From then on the document is checked with Mathlib, the inputs above included. A document that imports something itself keeps its own imports.
Run one original input at a time while the integration is being tested. Optional experiments below deliberately leave a proof unfinished or false: restore the working version before proceeding. The tutorial itself contains complete proofs, with no sorry.

1. Expressions, types, and evaluation

Lean can evaluate programs as well as check proofs. #eval evaluates an expression; #check reports its type. A type annotation (expression : Type) makes the intended number system explicit. Types affect the meaning of operations.
A computation, not a proof: 2 + 3·4 in the natural numbers.
#eval (2 + 3 * 4 : Nat)
14
In plain words: multiplication before addition, as usual: 14.
The type of 2 + 3, not its value.
#check (2 + 3 : Nat)
2 + 3 : Nat
In plain words: 2 + 3 is a natural number (Nat); Lean did not compute it.
3 − 5 in the natural numbers.
#eval (3 - 5 : Nat)
0
In plain words: ℕ has no negatives, so subtraction stops at zero: 0.
The same 3 − 5, in the integers (Int, ℤ).
#eval (3 - 5 : Int)
-2
In plain words: the number system decides what − means: here, −2.
1/3 + 1/6, exactly, in the rationals (Rat, ℚ).
#eval ((1 : Rat) / 3 + (1 : Rat) / 6)
(1 : Rat)/2
In plain words: 1/2, an exact fraction, with no rounding.

2. Definitions and reusable names

A definition, not a proof: the function that doubles a natural number. Read (n : Nat) as “n is a natural number”, the next : Nat as the result type, and := as “is defined to be”.
def l101_double (n : Nat) : Nat := n + n
Definition accepted: l101_double
In plain words: l101_double now names this function; it is applied by writing it before its argument.
The double of 7.
#eval l101_double 7
14
In plain words: 14: the definition does what was intended.
The type of l101_double.
#check l101_double
l101_double (n : Nat) : Nat
In plain words: a function from natural numbers to natural numbers, ℕ → ℕ.
Names beginning with l101_ belong to this tutorial. Refer to a Lean definition or theorem by its name; a Workspace CAS result label is not a Lean proof term. When experimenting, edit an existing definition or choose a fresh name rather than declaring the same name twice.

3. Your first theorem: statement, proof, goal

theorem name : statement := by starts a tactic proof. A tactic is an instruction that transforms or solves a goal. In Lean’s goal display, assumptions appear above ⊢; the statement still to prove appears after it.
A first theorem: n + 0 = n for every natural number n. rfl proves an equality whose two sides compute to the same thing.
theorem l101_add_zero (n : Nat) : n + 0 = n := by
  rfl
Proof checked: l101_add_zero
theorem l101_add_zero (n : Nat) : n + 0 = n := by
n : Nat ⊢ n + 0 = n
rfl
No goals
In plain words: adding zero gives the number back, from how addition is defined.
A theorem about the function above: the double of 3 is 6.
theorem l101_double_three : l101_double 3 = 6 := by
  rfl
Proof checked: l101_double_three
theorem l101_double_three : l101_double 3 = 6 := by
⊢ l101_double 3 = 6
rfl
No goals
In plain words: Lean unfolded the definition, computed 3 + 3, and found 6.
Try: change 6 to 7 in the preceding statement. The proof should fail. Restore 6. A failed tactic says this proposed proof did not work; it does not, by itself, prove the statement false.

4. Assumptions and implications

Prop is the type of propositions. A parameter (h : P) is evidence that P holds. exact h closes a goal when h proves exactly the required proposition.
If P holds, then P holds.
theorem l101_assumption (P : Prop) (h : P) : P := by
  exact h
Proof checked: l101_assumption
theorem l101_assumption (P : Prop) (h : P) : P := by
P : Prop h : P ⊢ P
exact h
No goals
In plain words: a claim that is among the hypotheses is proved by pointing at it.
P implies P. intro h assumes P and names the assumption h; watch it move above ⊢.
theorem l101_identity (P : Prop) : P → P := by
  intro h
  exact h
Proof checked: l101_identity
theorem l101_identity (P : Prop) : P → P := by
P : Prop ⊢ P → P
intro h
P : Prop h : P ⊢ P
exact h
No goals
In plain words: to prove an implication, assume its premise and prove its conclusion.
Try: temporarily leave only := by at the end of this theorem. Expect an unfinished proof with its initial goal. Restore the two proof lines. sorry is a placeholder for missing evidence, not a completed proof.

5. Several goals: “and”, branches, and “or”

A conjunction P ∧ Q requires both parts. constructor creates two goals. A bullet · opens a branch for one goal. Indentation matters. Given h : P ∧ Q, h.1 proves P and h.2 proves Q.
A proof with two branches: if P and Q both hold, then Q and P both hold.
theorem l101_swap_and (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  constructor
  · exact h.2
  · exact h.1
Proof checked: l101_swap_and
theorem l101_swap_and (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
P Q : Prop h : P ∧ Q ⊢ Q ∧ P
constructor
case left P Q : Prop h : P ∧ Q ⊢ Q case right P Q : Prop h : P ∧ Q ⊢ P
· exact h.2
P Q : Prop h : P ∧ Q ⊢ P
· exact h.1
No goals
In plain words: the order in “P and Q” does not matter; each part of the conclusion comes from the matching part of h.
If P holds, then “P or Q” holds, whatever Q is. left chooses to prove the left alternative.
theorem l101_choose_left (P Q : Prop) (h : P) : P ∨ Q := by
  left
  exact h
Proof checked: l101_choose_left
theorem l101_choose_left (P Q : Prop) (h : P) : P ∨ Q := by
P Q : Prop h : P ⊢ P ∨ Q
left
P Q : Prop h : P ⊢ P
exact h
No goals
In plain words: to prove “P or Q”, prove one of them; right would choose Q.
Try: omit the second branch of l101_swap_and. Expect P to remain unproved. Restore it before continuing. No remaining goals at an intermediate branch is not by itself the final theorem’s proof status; use the theorem badge too.

6. Rewriting and simplification

rw [h] uses an equality to replace one side by the other. simp repeatedly applies known simplification rules. Supplying a definition inside its brackets lets it unfold that definition as part of simplification.
If a = b, then a + 1 = b + 1.
theorem l101_rewrite (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]
Proof checked: l101_rewrite
theorem l101_rewrite (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
a b : Nat h : a = b ⊢ a + 1 = b + 1
rw [h]
No goals
In plain words: equals may be replaced by equals: after rw [h] both sides read b + 1.
The double of n, plus 0, equals n + n.
theorem l101_simplify (n : Nat) : l101_double n + 0 = n + n := by
  simp [l101_double]
Proof checked: l101_simplify
theorem l101_simplify (n : Nat) : l101_double n + 0 = n + n := by
n : Nat ⊢ l101_double n + 0 = n + n
simp [l101_double]
No goals
In plain words: unfolding the definition gives n + n + 0, and simplification drops the + 0.
Try: replace the last proof with unfold l101_double followed by simp, on separate indented lines. Compare the intermediate goal with the one-step proof.

7. Exact arithmetic and polynomial identities

Mathlib supplies tactics for common mathematical arguments. norm_num proves concrete numerical facts; ring proves polynomial identities by normalization. These tactics construct evidence Lean checks.
A theorem, where section 1 had a computation: 1/3 + 1/6 = 1/2 in ℚ.
theorem l101_fraction : (1 / 3 : ℚ) + 1 / 6 = 1 / 2 := by
  norm_num
Proof checked: l101_fraction
theorem l101_fraction : (1 / 3 : ℚ) + 1 / 6 = 1 / 2 := by
⊢ 1 / 3 + 1 / 6 = 1 / 2
norm_num
No goals
In plain words: the equality is proved, not just computed.
(x + 1)² = x² + 2x + 1 for every real x.
theorem l101_square (x : ℝ) : (x + 1)^2 = x^2 + 2*x + 1 := by
  ring
Proof checked: l101_square
theorem l101_square (x : ℝ) : (x + 1)^2 = x^2 + 2*x + 1 := by
x : ℝ ⊢ (x + 1) ^ 2 = x ^ 2 + 2 * x + 1
ring
No goals
In plain words: ring checks the algebra itself; no value of x was tried.
(x − y)(x + y) = x² − y² for all real x and y; a long statement may span several lines of one input.
theorem l101_difference_of_squares (x y : ℝ) :
    (x - y) * (x + y) = x^2 - y^2 := by
  ring
Proof checked: l101_difference_of_squares
theorem l101_difference_of_squares (x y : ℝ) :
    (x - y) * (x + y) = x^2 - y^2 := by
x y : ℝ ⊢ (x - y) * (x + y) = x ^ 2 - y ^ 2
ring
No goals
In plain words: the difference of two squares, for all real x and y.
Try: change the coefficient 2 to 3 in l101_square. The identity is no longer true for every x, and ring will not prove it. Restore 2.

8. Inequalities: choose the number system

omega handles many goals involving linear arithmetic over the integers. linarith combines linear equalities and inequalities, here over the reals. Keep the assumptions explicit.
If n ≥ 3, then n + 2 ≥ 5, for natural numbers.
theorem l101_nat_bound (n : Nat) (h : n ≥ 3) : n + 2 ≥ 5 := by
  omega
Proof checked: l101_nat_bound
theorem l101_nat_bound (n : Nat) (h : n ≥ 3) : n + 2 ≥ 5 := by
n : ℕ h : n ≥ 3 ⊢ n + 2 ≥ 5
omega
No goals
In plain words: adding 2 to a number at least 3 gives at least 5.
If x ≥ 3, then 2x + 1 ≥ 7, for real numbers.
theorem l101_real_bound (x : ℝ) (h : x ≥ 3) : 2*x + 1 ≥ 7 := by
  linarith
Proof checked: l101_real_bound
theorem l101_real_bound (x : ℝ) (h : x ≥ 3) : 2*x + 1 ≥ 7 := by
x : ℝ h : x ≥ 3 ⊢ 2 * x + 1 ≥ 7
linarith
No goals
In plain words: doubling gives at least 6, and adding 1 at least 7.
Try: strengthen the conclusion of the real theorem to 2*x + 1 ≥ 8. The given hypothesis is insufficient. Change the hypothesis as well if you want a valid stronger theorem.

9. Existence: supply a witness

To prove ∃ n : Nat, n > 10, give one suitable n and prove its property. refine ⟨11, ?_⟩ supplies 11 and leaves a goal where the question-mark placeholder sits. The next tactic must close that goal.
There is a natural number greater than 10.
theorem l101_witness : ∃ n : Nat, n > 10 := by
  refine ⟨11, ?_⟩
  norm_num
Proof checked: l101_witness
theorem l101_witness : ∃ n : Nat, n > 10 := by
⊢ ∃ n, n > 10
refine ⟨11, ?_⟩
⊢ 11 > 10
norm_num
No goals
In plain words: 11 is one, so one exists. Lean needed the number; then it checked 11 > 10.
This is also a useful CAS handoff pattern: a computation can suggest a witness, but Lean must still verify its required property. A suggested value is not automatically proof.

10. A readable chain of equalities

calc lays out a chain. Each equality needs a justification. The underscore denotes the previous expression in the chain. A theorem proved earlier can be used by name, with its arguments.
(x + 1)² − 1 = x² + 2x for every real x, as a chain of two equalities; the first cites l101_square from section 7.
theorem l101_square_shift (x : ℝ) : (x + 1)^2 - 1 = x^2 + 2*x := by
  calc
    (x + 1)^2 - 1 = (x^2 + 2*x + 1) - 1 := by rw [l101_square]
    _ = x^2 + 2*x := by ring
Proof checked: l101_square_shift
theorem l101_square_shift (x : ℝ) : (x + 1)^2 - 1 = x^2 + 2*x := by
x : ℝ ⊢ (x + 1) ^ 2 - 1 = x ^ 2 + 2 * x
calc
    (x + 1)^2 - 1 = (x^2 + 2*x + 1) - 1 := by rw [l101_square]
    _ = x^2 + 2*x := by ring
No goals
In plain words: the identity holds for every real x, and the proof cites an earlier theorem by name, as one cites a lemma.

11. Induction: prove all natural numbers at once

Induction gives a base case and a successor case. For the successor, the induction hypothesis records what has already been established for n. Here we deliberately prove a familiar fact by induction to inspect that structure.
0 + n = n for every natural number n, by induction: a base case, 0, and a step from n to n + 1 with the induction hypothesis ih. In the step, congrArg Nat.succ ih adds 1 to both sides of ih, and simpa matches the result with the goal.
theorem l101_zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simpa only [Nat.add_succ] using congrArg Nat.succ ih
Proof checked: l101_zero_add
theorem l101_zero_add (n : Nat) : 0 + n = n := by
n : ℕ ⊢ 0 + n = n
induction n with
  | zero => rfl
  | succ n ih =>
    simpa only [Nat.add_succ] using congrArg Nat.succ ih
No goals
In plain words: it holds for 0, and whenever it holds for n it holds for n + 1, so it holds for all n. Unlike n + 0 = n in section 3, it is not true by mere computation: Lean’s addition works through its second argument.
Compare the mathematical argument with the generated trace. Some nested tactic constructions appear as one compound step; a visual line is not necessarily one Lean step.

12. Mini-project: explore with CAS, certify with Lean

We will factor x² − 1. The variables named x in the two engines do not share a hidden value or assumption; the Lean statement below fixes the domain to ℝ explicitly.
A SymPy computation inside the Lean document: factor x² − 1. Its x shares nothing with a Lean x.
factor(x**2 - 1)
SymPy
(x - 1)*(x + 1)
In plain words: SymPy’s factorization is a suggestion; nothing about it is checked yet.
The claim that factorization makes, typed by hand: x² − 1 = (x − 1)(x + 1) for every real x.
theorem l101_factor (x : ℝ) : x^2 - 1 = (x - 1) * (x + 1) := by
  ring
Proof checked: l101_factor
theorem l101_factor (x : ℝ) : x^2 - 1 = (x - 1) * (x + 1) := by
x : ℝ ⊢ x ^ 2 - 1 = (x - 1) * (x + 1)
ring
No goals
In plain words: the factorization is correct for every real x, now established by Lean.
The Workspace can also write the theorem. Right-click the SymPy input line above (the input, not its result) and choose Use as Lean candidate:
The right-click menu on the SymPy line factor(x**2 - 1), with Use as Lean candidate highlighted
A new Lean input appears below that line, written by the Workspace, not by you: the equation the result states, over the reals, a proof to try, and a note of where it came from (the CAS, its input, and the assumptions on the variables). Enter checks it. The CAS result is not trusted; Lean’s badge is the verdict. Here it is, checked:
The candidate cas_candidate_1 written below the SymPy line: x^2 - 1 = (x - 1) * (x + 1) over the reals, proved by ring; Proof checked, the goal, ring, No goals
Try the interleaved presentation: right-click the generated theorem header and choose Insert CAS computation here. Type factor(x**2 - 1) and run it. Then recheck the generated ring step. This places exploration between proof steps; it does not make a CAS answer part of Lean’s trusted proof.
Candidates cover radicals too: √8 = 2√2. The Lean input under the SymPy line was written by the Workspace (right-click the input line, Use as Lean candidate); Real.sqrt is Mathlib’s square root.
sqrt(8)
SymPy
2*sqrt(2)
Candidate from the SymPy line above: sqrt(8). Lean’s badge is the verdict; the CAS result is not trusted.
-- candidate from the sympy line: sqrt(8)
theorem cas_candidate_1 : Real.sqrt 8 = 2 * Real.sqrt 2 := by
  rw [show (8 : ℝ) = 2 ^ 2 * 2 by norm_num, Real.sqrt_mul (by norm_num), Real.sqrt_sq (by norm_num)]
Proof checked: cas_candidate_1
theorem cas_candidate_1 : Real.sqrt 8 = 2 * Real.sqrt 2 := by
⊢ √8 = 2 * √2
rw [show (8 : ℝ) = 2 ^ 2 * 2 by norm_num, Real.sqrt_mul (by norm_num), Real.sqrt_sq (by norm_num)]
No goals
In plain words: √8 = 2√2 is proved by Lean; SymPy’s simplification was the suggestion.
A candidate with a side condition: (x² − 1)/(x − 1) = x + 1 holds only where x ≠ 1, and the theorem the Workspace wrote says so, as the hypothesis h1 : x - 1 ≠ 0.
cancel((x**2 - 1)/(x - 1))
SymPy
x + 1
Candidate from the SymPy line above: cancel((x**2 - 1)/(x - 1)); assumptions x : ℝ, x - 1 ≠ 0. Lean’s badge is the verdict; the CAS result is not trusted.
-- candidate from the sympy line: cancel((x**2 - 1)/(x - 1))
theorem cas_candidate_2 (x : ℝ) (h1 : x - 1 ≠ 0) : (x^2 - 1) / (x - 1) = x + 1 := by
  field_simp
  ring
Proof checked: cas_candidate_2
theorem cas_candidate_2 (x : ℝ) (h1 : x - 1 ≠ 0) : (x^2 - 1) / (x - 1) = x + 1 := by
x : ℝ h1 : x - 1 ≠ 0 ⊢ (x ^ 2 - 1) / (x - 1) = x + 1
field_simp
x : ℝ h1 : x - 1 ≠ 0 ⊢ x ^ 2 - 1 = (x - 1) * (x + 1)
ring
No goals
In plain words: the cancellation is correct for every real x except 1. SymPy’s answer does not say so; the theorem does.
1 is a root of x² − 1, using the factorization theorem by name.
theorem l101_root_one : (1 : ℝ)^2 - 1 = 0 := by
  rw [l101_factor]
  norm_num
Proof checked: l101_root_one
theorem l101_root_one : (1 : ℝ)^2 - 1 = 0 := by
⊢ 1 ^ 2 - 1 = 0
rw [l101_factor]
⊢ (1 - 1) * (1 + 1) = 0
norm_num
No goals
In plain words: one factor is zero, so the product is zero.
Exercise: add a new theorem named l101_root_minus_one stating (-1 : ℝ)^2 - 1 = 0. Adapt the two proof steps above. Then try replacing 0 by 1: Lean should reject the proposed proof.

13. Reading results and continuing

Proof checked applies to the checked formal statement. Proof incomplete means work remains. Check failed calls for inspecting the diagnostic. A changed source or dependency requires a new check; a saved result on reopening is historical evidence. The Workspace integration is still being tested, so report any mismatch between a summary and its generated goals.
Save this as an ordinary .eai document. Reopening should preserve the prose, original inputs, generated results and CAS regions without checking automatically. Recheck explicitly when you want current evidence.
A small vocabulary goes a long way: def, theorem, #check, #eval; then rfl, intro, exact, constructor, rw, simp, norm_num, ring, omega and linarith. Choose a tactic for the kind of goal you have, and inspect the new goal before continuing.
Further reading: Theorem Proving in Lean 4 for the language and proofs, and Mathematics in Lean for mathematical examples with Mathlib. These are complementary to the Workspace’s generated-region presentation.