Proofs

Express facts as types and proofs as values using theorem and Prop
Prove equalities and arithmetic facts with rfl, omega, and simp
Use decide to check concrete decidable propositions at compile time
Structure multi-step proofs with have, calc, and induction

Lean is not just a programming language: it is a proof assistant
The same type system that checks your data shapes can check mathematical facts

Propositions are Types

#check (1 + 1 = 2)
#check (5 > 3)
#check True
#check False

1 + 1 = 2 : Prop
5 > 3 : Prop
True : Prop
False : Prop

A proposition is a claim that may be true or false
In Lean, propositions are types: 1 + 1 = 2 has type Prop
Prop is the type of all logical claims
- Like Python's bool but checked by the compiler, not at runtime
True and False are also Prop values in the prelude

Proofs are Values

theorem onePlusOne : 1 + 1 = 2 := by rfl
theorem concatStr : "hi" ++ "!" = "hi!" := by rfl
#check @onePlusOne

onePlusOne : 1 + 1 = 2

A proof term is a value whose type is a proposition
theorem is like def but the value being defined is a proof
- theorem onePlusOne : 1 + 1 = 2 says "define a proof that 1 + 1 = 2"
by rfl is a tactic: a command that constructs a proof automatically
- rfl stands for "reflexivity": both sides reduce to the same value
#check @onePlusOne shows the type of the proof (the proposition itself)
- In Lean, some arguments are implicit: the type-checker infers them automatically rather than requiring the caller to supply them
- @ makes all implicit arguments explicit so #check shows the full type signature
- For onePlusOne, which has no implicit arguments, the output is the same either way
- This is like checking the type of a function with #check

When `rfl` Fails

-- rfl only works when both sides reduce to the same value
theorem wrong : 1 + 1 = 3 := by rfl

rfl_fails_err.lean:2:32: error: Tactic `rfl` failed: The left-hand side
  1 + 1
is not definitionally equal to the right-hand side
  3

⊢ 1 + 1 = 3

rfl only works when both sides reduce to the same value by computation
1 + 1 = 3 is false, so rfl fails with a type mismatch error
- The error shows what rfl proved (2 = 2) vs. what was needed (1 + 1 = 3)
That's a reasonable error message for once

The `omega` Tactic

theorem addComm (a b : Nat) : a + b = b + a := by omega
theorem gtZero (n : Nat) : 0 ≤ n := by omega
theorem noNegNat (n : Nat) : ¬(n < 0) := by omega
#check @addComm

addComm : ∀ (a b : Nat), a + b = b + a

omega is a decision procedure for linear arithmetic over Nat and Int
- It can prove any true fact that involves only +, -, comparisons, and constants
- Named after the Omega test from the 1990s
Works with universally quantified statements: (a b : Nat) means "for all a and b"
- Like Python's def parameters, but the function returns a proof, not a value
¬(n < 0) is the notation for "not n < 0" (type \neg)
- Lean rejects false arithmetic claims even if you ask nicely
rfl, omega, simp, decide, and induction are built into Lean 4: no import needed
- ring, linarith, and norm_num require import Mathlib.Tactic

The `simp` Tactic

theorem nilAppend : ([] : List Nat) ++ [1, 2] = [1, 2] := by simp
theorem appendNil (xs : List Nat) : xs ++ [] = xs := by simp
theorem listLen : [1, 2, 3].length = 3 := by simp

simp is a simplification tactic: it rewrites the goal using known lemmas
Knows basic list facts: empty list append, list length from literals
If simp leaves subgoals unsolved, combine it with omega: simp; omega
simp is powerful but opaque: you don't always see which rules it used
- For teaching purposes, prefer omega or rfl when they work

The `decide` Tactic

theorem mem3 : 3 ∈ [1, 2, 3, 4] := by decide
theorem mod7 : 22 % 7 = 1 := by decide
#check @mem3

mem3 : 3 ∈ [1, 2, 3, 4]

decide works for propositions that have a decidable algorithm
- List membership, modular arithmetic, boolean comparisons
Only works for concrete values, not for universally quantified statements
- 3 ∈ [1, 2, 3, 4] is decidable; ∀ n, n ∈ ns is not
- ∀ n, n ∈ ns means "every natural number is in ns", which is always false for a finite list
- More importantly, checking it would require testing infinitely many values of n; decide needs a finite computation, so there is no way to enumerate all Nat values
If decide times out, the proposition is probably too large to enumerate

Using `have`

theorem sumThree : 1 + 2 + 3 = 6 := by
  have h1 : 1 + 2 = 3 := by rfl
  have h2 : 3 + 3 = 6 := by rfl
  omega

have h : P := by tactic introduces an intermediate step named h
- Like a let binding but for propositions instead of values
- Once proved, h can be used as a hypothesis in the remaining proof
Breaking a proof into named steps makes it easier to read and debug
- Like decomposing a complex function into helper functions
omega at the end closes the goal using all available hypotheses
- After the two have steps, the proof state contains h1 : 1 + 2 = 3, h2 : 3 + 3 = 6, and the original goal 1 + 2 + 3 = 6
- omega treats all of these as a system of arithmetic constraints: substituting h1 into the goal gives 3 + 3 = 6, which is exactly h2

Hypotheses in Theorems

theorem positiveSum (a b : Int) (ha : 0 < a) (hb : 0 < b) : 0 < a + b := by omega
theorem bounded (n : Nat) (h : n < 10) : n ≤ 9 := by omega
#check @positiveSum

positiveSum : ∀ (a b : Int), 0 < a → 0 < b → 0 < a + b

A theorem can take propositions as parameters: (ha : 0 < a)
- These are hypotheses: facts the caller must supply
The source uses named-parameter syntax (ha : 0 < a), but the output of #check @positiveSum renders each hypothesis as →: ∀ (a b : ℤ), 0 < a → 0 < b → 0 < a + b
- This is why A → B in Lean means "given a proof of A, produce a proof of B"
- Function arrows and logical implication are the same thing in Lean
- Calling positiveSum with two integers and two proofs returns a proof of the conclusion

`calc` Chains

theorem sixViaTwo : 2 + 4 = 6 := by
  calc 2 + 4 = 4 + 2 := by omega
    _ = 6   := by rfl

theorem boundsCheck (n : Nat) (h : n ≤ 5) : n + n ≤ 10 := by
  calc n + n = 2 * n := by omega
    _ ≤ 2 * 5 := by omega
    _ = 10    := by rfl

calc is equational reasoning: a chain of steps where each links to the last
- _ on the left of each step refers to the right-hand side of the previous step
- Each step ends with := by tactic
Like a chain of assert a == b; assert b == c statements in Python
- But the compiler verifies that each link is correct
Use calc when you need different tactics for different steps, or when intermediate steps make the reasoning explicit
In sixViaTwo: rfl cannot prove 2 + 4 = 4 + 2 because rfl only succeeds when both sides reduce to the same value by computation — Lean evaluates 2 + 4 to 6 directly, but does not reorder addends, so 2 + 4 and 4 + 2 are not definitionally equal even though they name the same number
- omega handles the reordering; then 4 + 2 = 6 is definitionally true, so rfl closes it
boundsCheck shows a three-step chain mixing = and ≤: rewrite n + n as 2 * n, apply the hypothesis n ≤ 5 to bound it, then compute 2 * 5

Induction

theorem zeroAdd (n : Nat) : 0 + n = n := by
  induction n with
  | zero    => rfl
  | succ n ih => omega
#check @zeroAdd

zeroAdd : ∀ (n : Nat), 0 + n = n

In Lean, Nat is defined inductively: every natural number is either zero (0) or Nat.succ n (the successor of n, i.e., n + 1)
- 2 is Nat.succ (Nat.succ Nat.zero); 3 is one more succ on top of that
- This mirrors mathematical induction: to prove P n for all n, prove P 0 (base case) and prove that P n implies P (n + 1) (step case)
induction n with splits into cases matching the inductive definition of Nat
- zero case: prove the base claim
- succ n ih case: prove the step, using induction hypothesis ih
This is why the keyword is inductive: you can reason about types by induction
- The same principle that lets you recurse over lists works for proofs
omega in the succ case closes the goal using the induction hypothesis from context
- ih : 0 + n = n is a linear arithmetic fact; omega applies it automatically
- "Linear" means no variable is multiplied by another variable; the expression involves only addition, subtraction, and constants, which omega is designed to handle

Anonymous Proofs

example : 3 + 4 = 7 := by rfl
example (n : Nat) : n + 0 = n := by omega

example is an anonymous theorem: like theorem but with no name
- Useful for quick checks without cluttering the namespace
- Unlike #guard, which checks a value at runtime, example checks a type
Multiple example statements don't conflict even if they prove the same thing
- Named theorems like theorem foo : ... go into the namespace; two theorems with the same name produce a duplicate-definition error
- example has no name, so it never enters the namespace and cannot conflict
- Use them freely for exploration

The `ring` Tactic

import Mathlib.Tactic

theorem mulComm (a b : Nat) : a * b = b * a := by ring
theorem distribLeft (a b c : Nat) : a * (b + c) = a * b + a * c := by ring
theorem squareSum (a b : Int) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by ring
#check @mulComm

info: mathlib: checking out revision '41bee78e2cb1daff530b6838ca8c8f64a6dd898a'
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
Attempting to download 8107 file(s) from leanprover-community/mathlib4 cache

Downloaded: 1 file(s) [attempted 1/8107 = 0%, 106 KB/s], Decompressed: 0[K
Downloaded: 84 file(s) [attempted 84/8107 = 1%, 1495 KB/s], Decompressed: 1[K
Downloaded: 150 file(s) [attempted 150/8107 = 1%, 628 KB/s], Decompressed: 64[K
Downloaded: 220 file(s) [attempted 220/8107 = 2%, 3033 KB/s], Decompressed: 134[K
Downloaded: 280 file(s) [attempted 280/8107 = 3%, 331 KB/s], Decompressed: 200[K
Downloaded: 350 file(s) [attempted 350/8107 = 4%, 64 KB/s], Decompressed: 260[K
Downloaded: 409 file(s) [attempted 409/8107 = 5%, 88 KB/s], Decompressed: 331[K
Downloaded: 449 file(s) [attempted 449/8107 = 5%, 1088 KB/s], Decompressed: 399[K
Downloaded: 509 file(s) [attempted 509/8107 = 6%, 785 KB/s], Decompressed: 449[K
Downloaded: 552 file(s) [attempted 552/8107 = 6%, 340 KB/s], Decompressed: 449[K
Downloaded: 617 file(s) [attempted 617/8107 = 7%, 280 KB/s], Decompressed: 509[K
Downloaded: 679 file(s) [attempted 679/8107 = 8%, 860 KB/s], Decompressed: 579[K
Downloaded: 749 file(s) [attempted 749/8107 = 9%, 293 KB/s], Decompressed: 659[K
Downloaded: 809 file(s) [attempted 809/8107 = 9%, 3505 KB/s], Decompressed: 729[K
Downloaded: 869 file(s) [attempted 869/8107 = 10%, 391 KB/s], Decompressed: 789[K
Downloaded: 929 file(s) [attempted 929/8107 = 11%, 1244 KB/s], Decompressed: 849[K
Downloaded: 979 file(s) [attempted 979/8107 = 12%, 1890 KB/s], Decompressed: 899[K
Downloaded: 1028 file(s) [attempted 1028/8107 = 12%, 178 KB/s], Decompressed: 999[K
Downloaded: 1098 file(s) [attempted 1098/8107 = 13%, 110 KB/s], Decompressed: 1068[K
Downloaded: 1168 file(s) [attempted 1168/8107 = 14%, 1145 KB/s], Decompressed: 1098[K
Downloaded: 1228 file(s) [attempted 1228/8107 = 15%, 272 KB/s], Decompressed: 1158[K
Downloaded: 1288 file(s) [attempted 1288/8107 = 15%, 833 KB/s], Decompressed: 1208[K
Downloaded: 1358 file(s) [attempted 1358/8107 = 16%, 1474 KB/s], Decompressed: 1258[K
Downloaded: 1417 file(s) [attempted 1417/8107 = 17%, 1035 KB/s], Decompressed: 1318[K
Downloaded: 1477 file(s) [attempted 1477/8107 = 18%, 258 KB/s], Decompressed: 1388[K
Downloaded: 1557 file(s) [attempted 1557/8107 = 19%, 420 KB/s], Decompressed: 1457[K
Downloaded: 1627 file(s) [attempted 1627/8107 = 20%, 745 KB/s], Decompressed: 1517[K
Downloaded: 1687 file(s) [attempted 1687/8107 = 20%, 530 KB/s], Decompressed: 1607[K
Downloaded: 1737 file(s) [attempted 1737/8107 = 21%, 563 KB/s], Decompressed: 1607[K
Downloaded: 1816 file(s) [attempted 1816/8107 = 22%, 1134 KB/s], Decompressed: 1741[K
Downloaded: 1886 file(s) [attempted 1886/8107 = 23%, 2001 KB/s], Decompressed: 1796[K
Downloaded: 1956 file(s) [attempted 1956/8107 = 24%, 994 KB/s], Decompressed: 1896[K
Downloaded: 2026 file(s) [attempted 2026/8107 = 24%, 3095 KB/s], Decompressed: 1956[K
Downloaded: 2086 file(s) [attempted 2086/8107 = 25%, 268 KB/s], Decompressed: 2046[K
Downloaded: 2155 file(s) [attempted 2155/8107 = 26%, 519 KB/s], Decompressed: 2116[K
Downloaded: 2225 file(s) [attempted 2225/8107 = 27%, 122 KB/s], Decompressed: 2155[K
Downloaded: 2295 file(s) [attempted 2295/8107 = 28%, 1752 KB/s], Decompressed: 2245[K
Downloaded: 2355 file(s) [attempted 2355/8107 = 29%, 918 KB/s], Decompressed: 2285[K
Downloaded: 2435 file(s) [attempted 2435/8107 = 30%, 257 KB/s], Decompressed: 2382[K
Downloaded: 2504 file(s) [attempted 2504/8107 = 30%, 2028 KB/s], Decompressed: 2421[K
Downloaded: 2554 file(s) [attempted 2554/8107 = 31%, 2276 KB/s], Decompressed: 2475[K
Downloaded: 2634 file(s) [attempted 2634/8107 = 32%, 73 KB/s], Decompressed: 2574[K
Downloaded: 2669 file(s) [attempted 2669/8107 = 32%, 1350 KB/s], Decompressed: 2574[K
Downloaded: 2723 file(s) [attempted 2723/8107 = 33%, 53 KB/s], Decompressed: 2634[K
Downloaded: 2774 file(s) [attempted 2774/8107 = 34%, 1113 KB/s], Decompressed: 2694[K
Downloaded: 2844 file(s) [attempted 2844/8107 = 35%, 558 KB/s], Decompressed: 2754[K
Downloaded: 2913 file(s) [attempted 2913/8107 = 35%, 311 KB/s], Decompressed: 2863[K
Downloaded: 2983 file(s) [attempted 2983/8107 = 36%, 415 KB/s], Decompressed: 2913[K
Downloaded: 3043 file(s) [attempted 3043/8107 = 37%, 219 KB/s], Decompressed: 2973[K
Downloaded: 3113 file(s) [attempted 3113/8107 = 38%, 176 KB/s], Decompressed: 3033[K
Downloaded: 3194 file(s) [attempted 3194/8107 = 39%, 880 KB/s], Decompressed: 3133[K
Downloaded: 3238 file(s) [attempted 3238/8107 = 39%, 746 KB/s], Decompressed: 3183[K
Downloaded: 3302 file(s) [attempted 3302/8107 = 40%, 1117 KB/s], Decompressed: 3222[K
Downloaded: 3382 file(s) [attempted 3382/8107 = 41%, 76 KB/s], Decompressed: 3322[K
Downloaded: 3442 file(s) [attempted 3442/8107 = 42%, 153 KB/s], Decompressed: 3382[K
Downloaded: 3512 file(s) [attempted 3512/8107 = 43%, 485 KB/s], Decompressed: 3442[K
Downloaded: 3582 file(s) [attempted 3582/8107 = 44%, 458 KB/s], Decompressed: 3512[K
Downloaded: 3631 file(s) [attempted 3631/8107 = 44%, 682 KB/s], Decompressed: 3512[K
Downloaded: 3689 file(s) [attempted 3689/8107 = 45%, 613 KB/s], Decompressed: 3582[K
Downloaded: 3741 file(s) [attempted 3741/8107 = 46%, 1332 KB/s], Decompressed: 3698[K
Downloaded: 3811 file(s) [attempted 3811/8107 = 47%, 587 KB/s], Decompressed: 3741[K
Downloaded: 3861 file(s) [attempted 3861/8107 = 47%, 185 KB/s], Decompressed: 3791[K
Downloaded: 3931 file(s) [attempted 3931/8107 = 48%, 410 KB/s], Decompressed: 3884[K
Downloaded: 4010 file(s) [attempted 4010/8107 = 49%, 570 KB/s], Decompressed: 3921[K
Downloaded: 4070 file(s) [attempted 4070/8107 = 50%, 1116 KB/s], Decompressed: 3970[K
Downloaded: 4150 file(s) [attempted 4150/8107 = 51%, 721 KB/s], Decompressed: 4030[K
Downloaded: 4230 file(s) [attempted 4230/8107 = 52%, 874 KB/s], Decompressed: 4090[K
Downloaded: 4289 file(s) [attempted 4289/8107 = 52%, 451 KB/s], Decompressed: 4160[K
Downloaded: 4348 file(s) [attempted 4348/8107 = 53%, 757 KB/s], Decompressed: 4160[K
Downloaded: 4399 file(s) [attempted 4399/8107 = 54%, 109 KB/s], Decompressed: 4250[K
Downloaded: 4459 file(s) [attempted 4459/8107 = 55%, 241 KB/s], Decompressed: 4250[K
Downloaded: 4549 file(s) [attempted 4549/8107 = 56%, 1940 KB/s], Decompressed: 4379[K
Downloaded: 4619 file(s) [attempted 4619/8107 = 56%, 221 KB/s], Decompressed: 4379[K
Downloaded: 4688 file(s) [attempted 4688/8107 = 57%, 386 KB/s], Decompressed: 4379[K
Downloaded: 4728 file(s) [attempted 4728/8107 = 58%, 424 KB/s], Decompressed: 4379[K
Downloaded: 4778 file(s) [attempted 4778/8107 = 58%, 154 KB/s], Decompressed: 4379[K
Downloaded: 4828 file(s) [attempted 4828/8107 = 59%, 2049 KB/s], Decompressed: 4549[K
Downloaded: 4908 file(s) [attempted 4908/8107 = 60%, 1384 KB/s], Decompressed: 4549[K
Downloaded: 4957 file(s) [attempted 4957/8107 = 61%, 290 KB/s], Decompressed: 4549[K
Downloaded: 5067 file(s) [attempted 5067/8107 = 62%, 361 KB/s], Decompressed: 4549[K
Downloaded: 5107 file(s) [attempted 5107/8107 = 62%, 1283 KB/s], Decompressed: 4549[K
Downloaded: 5187 file(s) [attempted 5187/8107 = 63%, 102 KB/s], Decompressed: 4808[K
Downloaded: 5257 file(s) [attempted 5257/8107 = 64%, 560 KB/s], Decompressed: 4808[K
Downloaded: 5304 file(s) [attempted 5304/8107 = 65%, 345 KB/s], Decompressed: 4808[K
Downloaded: 5377 file(s) [attempted 5377/8107 = 66%, 110 KB/s], Decompressed: 4808[K
Downloaded: 5417 file(s) [attempted 5417/8107 = 66%, 2043 KB/s], Decompressed: 4808[K
Downloaded: 5456 file(s) [attempted 5456/8107 = 67%, 255 KB/s], Decompressed: 4808[K
Downloaded: 5511 file(s) [attempted 5511/8107 = 67%, 244 KB/s], Decompressed: 4808[K
Downloaded: 5596 file(s) [attempted 5596/8107 = 69%, 1600 KB/s], Decompressed: 4808[K
Downloaded: 5692 file(s) [attempted 5692/8107 = 70%, 911 KB/s], Decompressed: 5157[K
Downloaded: 5736 file(s) [attempted 5736/8107 = 70%, 1227 KB/s], Decompressed: 5157[K
Downloaded: 5802 file(s) [attempted 5802/8107 = 71%, 819 KB/s], Decompressed: 5157[K
Downloaded: 5819 file(s) [attempted 5819/8107 = 71%, 66 KB/s], Decompressed: 5157[K
Downloaded: 5855 file(s) [attempted 5855/8107 = 72%, 1566 KB/s], Decompressed: 5157[K
Downloaded: 5935 file(s) [attempted 5935/8107 = 73%, 395 KB/s], Decompressed: 5157[K
Downloaded: 6015 file(s) [attempted 6015/8107 = 74%, 224 KB/s], Decompressed: 5157[K
Downloaded: 6045 file(s) [attempted 6045/8107 = 74%, 2584 KB/s], Decompressed: 5157[K
Downloaded: 6085 file(s) [attempted 6085/8107 = 75%, 342 KB/s], Decompressed: 5157[K
Downloaded: 6164 file(s) [attempted 6164/8107 = 76%, 798 KB/s], Decompressed: 5157[K
Downloaded: 6235 file(s) [attempted 6235/8107 = 76%, 1147 KB/s], Decompressed: 5157[K
Downloaded: 6274 file(s) [attempted 6274/8107 = 77%, 2123 KB/s], Decompressed: 5157[K
Downloaded: 6344 file(s) [attempted 6344/8107 = 78%, 412 KB/s], Decompressed: 5656[K
Downloaded: 6424 file(s) [attempted 6424/8107 = 79%, 668 KB/s], Decompressed: 5656[K
Downloaded: 6474 file(s) [attempted 6474/8107 = 79%, 1267 KB/s], Decompressed: 5656[K
Downloaded: 6553 file(s) [attempted 6553/8107 = 80%, 89 KB/s], Decompressed: 5656[K
Downloaded: 6603 file(s) [attempted 6603/8107 = 81%, 200 KB/s], Decompressed: 5656[K
Downloaded: 6653 file(s) [attempted 6653/8107 = 82%, 75 KB/s], Decompressed: 5656[K
Downloaded: 6693 file(s) [attempted 6693/8107 = 82%, 77 KB/s], Decompressed: 5656[K
Downloaded: 6745 file(s) [attempted 6745/8107 = 83%, 2090 KB/s], Decompressed: 5656[K
Downloaded: 6783 file(s) [attempted 6783/8107 = 83%, 722 KB/s], Decompressed: 5656[K
Downloaded: 6853 file(s) [attempted 6853/8107 = 84%, 3435 KB/s], Decompressed: 5656[K
Downloaded: 6902 file(s) [attempted 6902/8107 = 85%, 1909 KB/s], Decompressed: 5656[K
Downloaded: 6972 file(s) [attempted 6972/8107 = 85%, 434 KB/s], Decompressed: 5656[K
Downloaded: 7052 file(s) [attempted 7052/8107 = 86%, 1816 KB/s], Decompressed: 5656[K
Downloaded: 7092 file(s) [attempted 7092/8107 = 87%, 470 KB/s], Decompressed: 5656[K
Downloaded: 7152 file(s) [attempted 7152/8107 = 88%, 1631 KB/s], Decompressed: 5656[K
Downloaded: 7232 file(s) [attempted 7232/8107 = 89%, 4322 KB/s], Decompressed: 5656[K
Downloaded: 7331 file(s) [attempted 7331/8107 = 90%, 1465 KB/s], Decompressed: 5656[K
Downloaded: 7381 file(s) [attempted 7381/8107 = 91%, 458 KB/s], Decompressed: 6304[K
Downloaded: 7451 file(s) [attempted 7451/8107 = 91%, 152 KB/s], Decompressed: 6304[K
Downloaded: 7521 file(s) [attempted 7521/8107 = 92%, 158 KB/s], Decompressed: 6304[K
Downloaded: 7591 file(s) [attempted 7591/8107 = 93%, 230 KB/s], Decompressed: 6304[K
Downloaded: 7690 file(s) [attempted 7690/8107 = 94%, 298 KB/s], Decompressed: 6304[K
Downloaded: 7750 file(s) [attempted 7750/8107 = 95%, 2563 KB/s], Decompressed: 6304[K
Downloaded: 7810 file(s) [attempted 7810/8107 = 96%, 289 KB/s], Decompressed: 6304[K
Downloaded: 7850 file(s) [attempted 7850/8107 = 96%, 279 KB/s], Decompressed: 6304[K
Downloaded: 7920 file(s) [attempted 7920/8107 = 97%, 1263 KB/s], Decompressed: 6304[K
Downloaded: 7970 file(s) [attempted 7970/8107 = 98%, 147 KB/s], Decompressed: 6304[K
Downloaded: 7979 file(s) [attempted 7979/8107 = 98%, 846 KB/s], Decompressed: 6304[K
Downloaded: 8074 file(s) [attempted 8074/8107 = 99%, 2421 KB/s], Decompressed: 6304[K
Downloaded: 8099 file(s) [attempted 8099/8107 = 99%, 1002 KB/s], Decompressed: 6304[K
Downloaded: 8107 file(s) [attempted 8107/8107 = 100%, 1002 KB/s], Decompressed: 6304[K
Decompressed 8107 file(s)
Already decompressed 8472 file(s)
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
No files to download
Already decompressed 8472 file(s)
mulComm : ∀ (a b : ℕ), a * b = b * a

A ring is an algebraic structure with addition and multiplication that obeys familiar rules: commutativity, associativity, distributivity, and identity elements (0 and 1)
- Integers, natural numbers, and polynomials are all rings
ring proves identities in commutative rings: expressions involving +, *, -, and numeric literals
- omega handles linear arithmetic; ring handles polynomial algebra
- Not a Lean 4 built-in: requires import Mathlib.Tactic
mulComm shows multiplication commutativity
- omega cannot prove this because it involves variable * variable
squareSum expands (a + b) * (a + b) symbolically
- Like calling expand() in a computer algebra system: the system rewrites (a + b)^2 into a^2 + 2ab + b^2 symbolically
The boundary: use omega for anything linear (no variable × variable); use ring for polynomials

Why This Matters

-- Prove that byte values stay below 256 when each input is below 128
theorem safeByteAdd (a b : Nat) (ha : a < 128) (hb : b < 128) : a + b < 256 := by omega

-- Verify a hexadecimal constant matches its decimal value at compile time
theorem hexDecimal : 0xFF = 255 := by decide

-- Prove a list of valid HTTP status codes has the expected length
def successCodes : List Nat := [200, 201, 202, 204]
theorem fourSuccessCodes : successCodes.length = 4 := by decide

Lean's proof tactics can verify invariants at compile time, catching bugs before they reach runtime
omega proves that arithmetic stays within safe bounds given input constraints
- safeByteAdd guarantees that adding two sub-128 values never overflows a byte: this is a statement the compiler checks, not a runtime assertion that can be skipped
- Any caller that passes values outside the stated bounds will not type-check
decide verifies that named constants match their intended values
- A mismatch between 0xFF and 255 becomes a compile-time error rather than a latent bug discovered during a code review or test failure
decide also checks properties of small configuration tables
- If a new status code is added to successCodes without updating the count, fourSuccessCodes fails at build time rather than silently at runtime

Exercises

Fix: False Equality

-- Fix: this theorem is false
theorem wrong : 2 + 2 = 5 := by rfl

hint

2 + 2 = 5 is false; no tactic can prove it
Change the right-hand side to the correct value: 4

Fix: False Arithmetic Claim

-- Fix: this theorem is false; omega correctly rejects it
theorem claim (n : Nat) : n + 1 < n := by omega

hint

n + 1 < n is false for every natural number: omega correctly rejects it
Change the claim to something true, like n < n + 1

Fix: Wrong List Length

-- Fix: the list has the wrong length in this claim
theorem len3 : [1, 2, 3].length = 4 := by simp

hint

[1, 2, 3] has length 3, not 4
Change the expected length to 3 and simp will succeed

Fix: Element Not in List

-- Fix: 5 is not in this list
theorem mem : 5 ∈ [1, 2, 3] := by decide

hint

5 is not in [1, 2, 3]; decide will reject a false membership claim
Either add 5 to the list, or change the element to one that is already in the list

Fix: Wrong Intermediate Step

-- Fix: the intermediate step asserts the wrong value
theorem sumTwo : 10 + 20 = 30 := by
  have h : 10 + 20 = 31 := by rfl
  omega

hint

The have step claims 10 + 20 = 31, which is false
rfl will reject it — fix the claim to 10 + 20 = 30
Once the intermediate step is correct, omega can close the goal

Fix: False Arithmetic in Induction Exercise

-- Fix: this claim is false; omega correctly rejects it
theorem alwaysGrows (n : Nat) : n + 1 > n + 1 := by omega

hint

n + 1 > n + 1 says "strictly greater than itself", which is never true
Change the claim to n + 1 > n, which omega can prove directly

Write: Commutativity of Addition

-- Write: replace 'sorry' with the right tactic
theorem addComm (a b : Nat) : a + b = b + a := by
  sorry

#check @addComm

hint

Replace sorry with omega
omega handles commutativity of addition over natural numbers directly

Write: Double Equals Twice

-- Write: replace 'sorry' with the right tactic
theorem doubleEq (n : Nat) : n + n = 2 * n := by
  sorry

hint

Replace sorry with omega
n + n = 2 * n is a linear arithmetic fact; omega handles it

Write: Modular Arithmetic by `decide`

-- Write: replace 'sorry' with the right tactic
theorem mod5 : 17 % 5 = 2 := by
  sorry

hint

Replace sorry with decide
17 % 5 = 2 is a concrete numerical fact; decide verifies it by computation

Write: Empty List Append

-- Write: replace 'sorry' with the right tactic
theorem nilLeft : ([] : List Nat) ++ [1, 2] = [1, 2] := by
  sorry

hint

Replace sorry with simp
simp knows that [] ++ xs = xs and applies it automatically

Write: Two-Step `calc` Proof

-- Write: use calc to prove 3 + 4 = 7 in two steps
-- Step 1: 3 + 4 = 4 + 3  (by omega)
-- Step 2: 4 + 3 = 7      (by rfl)
theorem calcExample : 3 + 4 = 7 := by
  sorry

hint

Replace sorry with a calc block
Step 1: 3 + 4 = 4 + 3 := by omega
Step 2: _ = 7 := by rfl

Write: Zero Is a Lower Bound

-- Write: prove that 0 is less than or equal to any Nat
theorem geZero (n : Nat) : 0 ≤ n := by
  sorry

#check @geZero

hint

Replace sorry with omega
0 ≤ n for Nat is always true because Nat cannot be negative

Proofs

Propositions are Types

Proofs are Values

When rfl Fails

The omega Tactic

The simp Tactic

The decide Tactic

Using have

Hypotheses in Theorems

calc Chains

Induction

Anonymous Proofs

The ring Tactic

Why This Matters

Exercises

Fix: False Equality

Fix: False Arithmetic Claim

Fix: Wrong List Length

Fix: Element Not in List

Fix: Wrong Intermediate Step

Fix: False Arithmetic in Induction Exercise

Write: Commutativity of Addition

Write: Double Equals Twice

Write: Modular Arithmetic by decide

Write: Empty List Append

Write: Two-Step calc Proof

Write: Zero Is a Lower Bound

When `rfl` Fails

The `omega` Tactic

The `simp` Tactic

The `decide` Tactic

Using `have`

`calc` Chains

The `ring` Tactic

Write: Modular Arithmetic by `decide`

Write: Two-Step `calc` Proof