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

warning: /Users/gvwilson/l4py/proof/lakefile.lean:5:2: unknown 'PackageConfig' field 'name'
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: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✔ [4/24] Built Batteries.Data.String.Basic (239ms)
✔ [5/24] Built Cache.Lean (341ms)
✔ [6/24] Built Cache.Init (215ms)
✔ [7/24] Built Batteries.Data.Array.Match (458ms)
✔ [8/24] Built Batteries.Data.Array.Match:c.o (138ms)
✔ [9/24] Built Batteries.Data.String.Basic:c.o (283ms)
✔ [10/24] Built Cache.Lean:c.o (178ms)
✔ [11/24] Built Cache.Init:c.o (143ms)
✔ [12/24] Built Batteries.Data.String.Matcher (234ms)
✔ [13/24] Built Batteries.Tactic.OpenPrivate (508ms)
✔ [14/24] Built Batteries.Data.String.Matcher:c.o (105ms)
✔ [15/24] Built Batteries.Tactic.OpenPrivate:c.o (490ms)
✔ [16/24] Built Cache.IO (694ms)
✔ [17/24] Built Cache.Hashing (487ms)
✔ [18/24] Built Cache.IO:c.o (604ms)
✔ [19/24] Built Cache.Hashing:c.o (194ms)
✔ [20/24] Built Cache.Requests (902ms)
✔ [21/24] Built Cache.Main (555ms)
✔ [22/24] Built Cache.Main:c.o (290ms)
✔ [23/24] Built Cache.Requests:c.o (899ms)
✔ [24/24] Built cache:exe (866ms)
Decompressing 8544 already-cached file(s) (4 already decompressed)
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
No files to download
Decompressed 8544 already-cached file(s)
Completed successfully in 10057 ms!
Decompressing 367 already-cached file(s) (8181 already decompressed)
Current branch: HEAD
Using cache (Azure) from origin: (some leanprover-community/mathlib4)
No files to download
Decompressed 367 already-cached file(s)
Completed successfully in 1889 ms!
✔ [27/40] Built Batteries.Lean.Position (253ms)
✔ [28/40] Built Batteries.Tactic.Unreachable (298ms)
✔ [30/40] Built Batteries.Lean.Meta.Inaccessible (251ms)
✔ [31/40] Built Batteries.Tactic.Lint.Basic (447ms)
✔ [38/68] Built ImportGraph.Imports.ImportGraph (292ms)
✔ [40/68] Built ImportGraph.Lean.Environment (322ms)
✔ [41/68] Built Batteries.Tactic.Lint.Misc (623ms)
✔ [45/68] Built Batteries.Lean.Syntax (375ms)
✔ [46/68] Built ImportGraph.Graph.TransitiveClosure (322ms)
✔ [47/71] Built ImportGraph.Imports.Redundant (294ms)
✔ [48/71] Built Batteries.Tactic.Lint.TypeClass (433ms)
✔ [51/72] Built Batteries.Util.LibraryNote (665ms)
✔ [52/77] Built ImportGraph.Tools.ImportDiff (571ms)
✔ [53/80] Built ImportGraph.Imports.RequiredModules (636ms)
✔ [55/80] Built Qq.ForLean.ToExpr (446ms)
✔ [58/87] Built ImportGraph.Tools.RedundantImports (591ms)
✔ [59/87] Built Qq.ForLean.ReduceEval (478ms)
✔ [60/87] Built Qq.Typ (511ms)
✔ [61/89] Built Qq.ForLean.Do (443ms)
✔ [62/109] Built Batteries.Util.ProofWanted (918ms)
✔ [63/109] Built Qq.SortLocalDecls (404ms)
✔ [64/130] Built ImportGraph.Tools.MinImports (482ms)
✔ [65/130] Built Batteries.Tactic.Lint.Frontend (1.4s)
✔ [66/135] Built ImportGraph.Tools.FindHome (679ms)
✔ [67/135] Built Batteries.Lean.NameMapAttribute (455ms)
✔ [68/135] Built Batteries.Tactic.Lint.Simp (1.1s)
✔ [69/143] Built Batteries.Tactic.SeqFocus (552ms)
✔ [70/143] Built Batteries.Data.Nat.Basic (450ms)
✔ [71/151] Built Batteries.CodeAction.Deprecated (888ms)
✔ [72/151] Built Batteries.Lean.Expr (472ms)
✔ [73/169] Built ImportGraph.Tools (499ms)
✔ [74/169] Built Batteries.Tactic.Lint (443ms)
✔ [76/169] Built Batteries.Lean.TagAttribute (342ms)
✔ [77/171] Built Batteries.Lean.Except (378ms)
✔ [78/171] Built Batteries.Tactic.HelpCmd (1.8s)
✔ [105/171] Built Batteries.Linter.UnreachableTactic (690ms)
✔ [115/171] Built Batteries.Lean.AttributeExtra (355ms)
✔ [116/171] Built Batteries.Lean.Meta.UnusedNames (316ms)
✔ [118/173] Built Batteries.Util.ExtendedBinder (477ms)
✔ [121/185] Built Batteries.Tactic.Init (867ms)
✔ [122/186] Built Batteries.Tactic.Trans (1.7s)
✔ [124/186] Built Aesop.Script.Tactic (349ms)
✔ [125/194] Built Batteries.Tactic.Alias (1.2s)
✔ [134/194] Built Batteries.Control.Lemmas (408ms)
✔ [135/194] Built Aesop.Nanos (347ms)
✔ [138/194] Built Aesop.Script.GoalWithMVars (470ms)
✔ [139/194] Built Aesop.Index.DiscrTreeConfig (295ms)
✔ [140/197] Built Batteries.Linter.UnnecessarySeqFocus (832ms)
✔ [141/197] Built Batteries.Lean.MonadBacktrack (300ms)
✔ [142/199] Built Batteries.Tactic.Exact (472ms)
✔ [144/199] Built Batteries.Tactic.PermuteGoals (571ms)
✔ [145/209] Built Batteries.Control.LawfulMonadState (1.0s)
✔ [146/209] Built Batteries.Data.Array.Merge (852ms)
✔ [147/209] Built Aesop.Check (489ms)
✔ [148/209] Built Batteries.Linter (458ms)
✔ [149/213] Built Batteries.Logic (616ms)
✔ [152/213] Built Batteries.Data.Nat.Lemmas (769ms)
✔ [156/213] Built Aesop.Rule.Name (575ms)
✔ [166/219] Built Aesop.Util.UnorderedArraySet (386ms)
✔ [167/219] Built Aesop.Forward.LevelIndex (295ms)
✔ [168/228] Built Aesop.Options.Public (593ms)
✔ [169/228] Built Aesop.Script.OptimizeSyntax (540ms)
✔ [170/228] Built Aesop.Forward.PremiseIndex (394ms)
✔ [171/234] Built Batteries.Control.OptionT (454ms)
✔ [172/234] Built Aesop.Percent (338ms)
✔ [173/237] Built Batteries.Tactic.Basic (410ms)
✔ [174/237] Built Aesop.Forward.SlotIndex (323ms)
✔ [175/243] Built Qq.Macro (3.5s)
✔ [176/243] Built Aesop.Options.Internal (347ms)
✔ [177/243] Built Aesop.Util.UnionFind (467ms)
✔ [178/248] Built Aesop.RuleTac.RuleTerm (411ms)
✔ [179/248] Built Aesop.Util.Tactic (387ms)
✔ [180/249] Built Aesop.ElabM (463ms)
✔ [181/249] Built Aesop.Constants (290ms)
✔ [182/252] Built Aesop.Util.Unfold (533ms)
✔ [183/254] Built Batteries.Control.AlternativeMonad (696ms)
✔ [184/254] Built Batteries.Lean.Meta.Expr (312ms)
✔ [185/256] Built Batteries.Classes.Order (674ms)
✔ [186/256] Built Aesop.Util.OrderedHashSet (440ms)
✔ [187/256] Built Batteries.Lean.PersistentHashMap (359ms)
✔ [191/264] Built Batteries.Lean.PersistentHashSet (343ms)
✔ [192/274] Built Aesop.RuleTac.ElabRuleTerm (559ms)
✔ [193/289] Built Qq.Commands (854ms)
✔ [194/289] Built Batteries.Lean.Meta.DiscrTree (378ms)
✔ [195/289] Built Aesop.RuleSet.Name (382ms)
✔ [196/291] Built Batteries.Lean.Meta.Basic (507ms)
✔ [197/291] Built Batteries.Lean.HashSet (338ms)
✔ [198/291] Built Aesop.Util.Tactic.Unfold (652ms)
✔ [199/291] Built Qq.Delab (1.2s)
✔ [200/291] Built Aesop.Util.Basic (1.7s)
✔ [201/291] Built Batteries.Data.UInt (795ms)
✔ [202/291] Built Aesop.RuleSet.Filter (412ms)
✔ [203/291] Built Aesop.Search.Expansion.Simp (510ms)
✔ [204/291] Built Aesop.Exception (464ms)
✔ [205/291] Built Batteries.Control.ForInStep.Basic (413ms)
✔ [206/293] Built Batteries.Lean.Meta.SavedState (432ms)
✔ [207/293] Built Batteries.Lean.Meta.InstantiateMVars (539ms)
✔ [208/309] Built Aesop.Script.TacticState (416ms)
✔ [209/312] Built Qq.MetaM (487ms)
✔ [210/312] Built Aesop.Script.CtorNames (570ms)
✔ [211/328] Built Aesop.RuleTac.Forward.Basic (730ms)
✔ [212/328] Built Aesop.Frontend.Basic (413ms)
✔ [216/330] Built Aesop.EMap (796ms)
✔ [217/330] Built Aesop.Tracing (955ms)
✔ [218/330] Built Aesop.Forward.Substitution (863ms)
✔ [219/330] Built Qq.Simp (412ms)
✔ [220/330] Built Qq.MatchImpl (470ms)
✔ [223/339] Built Qq.AssertInstancesCommute (893ms)
✔ [224/339] Built Aesop.RulePattern.Cache (478ms)
✔ [225/345] Built Aesop.Index.Basic (634ms)
✔ [226/345] Built Plausible.Random (486ms)
✔ [227/347] Built Aesop.Util.Tactic.Ext (733ms)
✔ [228/347] Built Plausible.Attr (343ms)
✔ [229/348] Built Plausible.Shrinkable (426ms)
✔ [230/348] Built Aesop.Stats.Basic (1.2s)
✔ [231/353] Built Plausible.Gen (726ms)
✔ [232/353] Built Batteries.CodeAction.Attr (590ms)
✔ [233/353] Built Batteries.Tactic.Case (1.2s)
✔ [234/353] Built Aesop.Stats.Extension (412ms)
✔ [235/353] Built Aesop.Stats.File (459ms)
✔ [236/353] Built Aesop.BaseM (519ms)
✔ [237/353] Built Batteries.Data.Array.Basic (2.9s)
✔ [238/353] Built Plausible.DeriveShrinkable (1.3s)
✔ [240/353] Built Aesop.Util.EqualUpToIds (3.5s)
✔ [241/353] Built Batteries.CodeAction.Basic (757ms)
✔ [243/354] Built Plausible.Arbitrary (497ms)
✔ [244/354] Built Aesop.Stats.Report (595ms)
✔ [245/357] Built Batteries.Data.BinomialHeap.Basic (3.6s)
✔ [246/357] Built Plausible.ArbitraryFueled (272ms)
✔ [247/358] Built Aesop.Script.Util (392ms)
✔ [249/360] Built LeanSearchClient.Basic (289ms)
✔ [250/388] Built Aesop.RuleTac.GoalDiff (1.0s)
✔ [279/395] Built Plausible.Sampleable (605ms)
✔ [280/395] Built Batteries.CodeAction.Misc (1.6s)
✔ [286/395] Built Aesop.RulePattern (1.3s)
✔ [289/398] Built Aesop.Script.Step (785ms)
✔ [290/398] Built Batteries.Tactic.GeneralizeProofs (3.0s)
✔ [291/398] Built Batteries.Util.Cache (505ms)
✔ [292/398] Built Qq.Match (3.8s)
✔ [293/398] Built Plausible.Functions (613ms)
✔ [294/407] Built Aesop.Index.RulePattern (766ms)
✔ [295/407] Built Plausible.DeriveArbitrary (1.3s)
✔ [302/411] Built Aesop.Script.UScript (411ms)
✔ [303/411] Built Aesop.Script.ScriptM (502ms)
✔ [304/411] Built Batteries.Data.List.Basic (2.5s)
✔ [306/415] Built Aesop.Script.SScript (521ms)
✔ [307/415] Built Aesop.RuleTac.Basic (751ms)
✔ [313/415] Built Aesop.Forward.RuleInfo (959ms)
✔ [314/415] Built Qq (475ms)
✔ [315/415] Built LeanSearchClient.Syntax (1.6s)
✔ [320/424] Built Aesop.Script.Check (444ms)
✔ [331/452] Built Aesop.Search.Expansion.Basic (447ms)
✔ [332/452] Built Plausible.Testable (1.5s)
✔ [367/458] Built Aesop.Rule.Forward (466ms)
✔ [368/458] Built Batteries.Data.MLList.Basic (853ms)
✔ [369/458] Built Aesop.Script.UScriptToSScript (806ms)
✔ [370/458] Built Aesop.RuleTac.Tactic (692ms)
✔ [371/458] Built Batteries.CodeAction.Match (960ms)
✔ [374/469] Built Plausible.Tactic (603ms)
✔ [375/477] Built Batteries.Control.Nondet.Basic (510ms)
✔ [382/507] Built Aesop.Forward.Match.Types (518ms)
✔ [383/507] Built LeanSearchClient.LoogleSyntax (974ms)
✔ [408/526] Built Batteries.CodeAction (540ms)
✔ [409/526] Built ProofWidgets.Compat (456ms)
✔ [421/577] Built Aesop.Script.SpecificTactics (1.6s)
✔ [422/577] Built Plausible (423ms)
✔ [423/577] Built ProofWidgets.Util (592ms)
✔ [448/577] Built Aesop.Script.StructureStatic (830ms)
✔ [449/577] Built Aesop.RuleTac.Descr (447ms)
✔ [450/622] Built Aesop.Index.Forward (547ms)
✔ [451/622] Built LeanSearchClient (440ms)
✔ [452/622] Built Batteries.Classes.RatCast (372ms)
✔ [488/835] Built Aesop.RuleTac.Preprocess (464ms)
✔ [496/837] Built Aesop.Script.StructureDynamic (1.3s)
✔ [497/837] Built Aesop.Rule.Basic (423ms)
✔ [498/837] Built ProofWidgets.Component.Basic (707ms)
✔ [500/844] Built Aesop.RuleTac.Apply (693ms)
✔ [501/844] Built Batteries.Control.ForInStep.Lemmas (365ms)
✔ [502/913] Built Aesop.RuleTac.Cases (769ms)
✔ [503/913] Built ProofWidgets.Cancellable (758ms)
✔ [520/1199] Built Batteries.Tactic.Congr (769ms)
✔ [521/1199] Built Batteries.Data.List.Pairwise (553ms)
✔ [549/1364] Built Aesop.Rule (499ms)
✔ [550/1364] Built ProofWidgets.Component.MakeEditLink (543ms)
✔ [557/1365] Built Aesop.Script.Main (547ms)
✔ [558/1365] Built Batteries.Data.Fin.Basic (776ms)
✔ [565/1911] Built Aesop.Index (869ms)
✔ [567/2117] Built Aesop.RuleSet.Member (439ms)
✔ [573/2191] Built Aesop.Tree.UnsafeQueue (562ms)
✔ [599/2724] Built Batteries.Lean.HashMap (238ms)
✔ [601/2778] Built Aesop.Builder.Basic (499ms)
✔ [602/2781] Built Aesop.Forward.Match (1.2s)
✔ [603/2781] Built Batteries.Data.Fin.Lemmas (1.1s)
✔ [604/2808] Built Aesop.Builder.Constructors (568ms)
✔ [605/2808] Built Aesop.Builder.Tactic (654ms)
✔ [606/2808] Built Aesop.Builder.Apply (604ms)
✔ [607/2943] Built Aesop.Builder.Cases (496ms)
✔ [608/2943] Built Aesop.Builder.NormSimp (715ms)
✔ [619/2953] Built Aesop.Tree.Data.ForwardRuleMatches (451ms)
✔ [620/2953] Built Aesop.Builder.Unfold (771ms)
✔ [624/2959] Built ProofWidgets.Data.Html (2.4s)
✔ [626/2959] Built Aesop.Builder.Default (555ms)
✔ [628/2959] Built ProofWidgets.Component.HtmlDisplay (679ms)
✔ [629/2959] Built ProofWidgets.Presentation.Expr (835ms)
✔ [630/2959] Built Aesop.Builder.Forward (1.7s)
✔ [631/2959] Built ProofWidgets.Component.PenroseDiagram (974ms)
✔ [632/2959] Built ProofWidgets.Component.OfRpcMethod (841ms)
✔ [638/2959] Built Aesop.RuleTac.Forward (1.6s)
✔ [639/2959] Built ProofWidgets.Component.FilterDetails (665ms)
✔ [641/2959] Built ProofWidgets.Component.Panel.Basic (1.6s)
✔ [642/2959] Built Aesop.RuleTac (351ms)
✔ [643/2959] Built Aesop.RuleSet (2.2s)
✔ [644/2959] Built Aesop.Frontend.Extension.Init (290ms)
✔ [645/2959] Built Aesop.Frontend.RuleExpr (1.5s)
✔ [646/2959] Built Batteries.Data.List.Lemmas (4.7s)
✔ [649/2959] Built Aesop.Frontend.Extension (394ms)
✔ [650/2959] Built Aesop.Forward.State (3.3s)
✔ [651/2959] Built Aesop.Frontend.Attribute (609ms)
✔ [652/2959] Built Batteries.Data.List.Count (995ms)
✔ [653/2959] Built Aesop.Forward.State.Initial (487ms)
✔ [654/2959] Built Aesop.Frontend.Tactic (754ms)
✔ [655/2959] Built Aesop.Forward.State.ApplyGoalDiff (643ms)
✔ [656/2959] Built Aesop.Frontend.Command (1.0s)
✔ [657/2959] Built Aesop.BuiltinRules.Rfl (505ms)
✔ [658/2959] Built Aesop.BuiltinRules.Split (657ms)
✔ [660/2959] Built Aesop.Tree.Data (1.1s)
✔ [661/2959] Built Aesop.BuiltinRules.Ext (702ms)
✔ [662/2959] Built Aesop.BuiltinRules.Intros (692ms)
✔ [663/2959] Built Aesop.BuiltinRules.Assumption (782ms)
✔ [664/2959] Built Aesop.BuiltinRules.ApplyHyps (780ms)
✔ [665/2959] Built Aesop.BuiltinRules.DestructProducts (843ms)
✔ [666/2959] Built Aesop.BuiltinRules.Subst (663ms)
✔ [667/2959] Built Aesop.Search.Queue.Class (359ms)
✔ [668/2959] Built Aesop.Tree.RunMetaM (410ms)
✔ [669/2959] Built Aesop.Tree.Traversal (493ms)
✔ [670/2959] Built Aesop.BuiltinRules (444ms)
✔ [671/2959] Built Aesop.Tree.TreeM (705ms)
✔ [672/2959] Built Aesop.Search.Queue (543ms)
✔ [673/2959] Built Batteries.Data.List.Perm (1.4s)
✔ [674/2959] Built Aesop.Tree.State (585ms)
✔ [675/2959] Built Aesop.Tree.Free (605ms)
✔ [676/2959] Built Aesop.Tree.Tracing (987ms)
✔ [677/2959] Built Aesop.Tree.Stats (636ms)
✔ [678/2959] Built Aesop.Search.SearchM (792ms)
✔ [679/2959] Built Aesop.Forward.State.UpdateGoal (555ms)
✔ [680/2959] Built Aesop.Tree.ExtractProof (893ms)
✔ [681/2959] Built Aesop.Tree.ExtractScript (983ms)
✔ [682/2959] Built Aesop.Search.RuleSelection (424ms)
✔ [683/2959] Built Aesop.Tree.Check (833ms)
✔ [684/2959] Built Aesop.Tree.AddRapp (1.5s)
✔ [685/2959] Built Aesop.Saturate (3.3s)
✔ [686/2959] Built Aesop.Search.Expansion.Norm (1.3s)
✔ [687/2959] Built Aesop.Frontend.Saturate (487ms)
✔ [688/2959] Built Aesop.Frontend (285ms)
✔ [694/2959] Built Aesop.Search.Expansion (850ms)
✔ [695/2959] Built Aesop.Search.ExpandSafePrefix (445ms)
✔ [696/2959] Built Aesop.Search.Main (1.4s)
✔ [697/2959] Built Aesop.Main (492ms)
✔ [728/2959] Built Aesop (282ms)
ℹ [2958/2959] Built ring_proof (12s)
info: ring_proof.lean:6:0: mulComm : ∀ (a b : ℕ), a * b = b * a
Build completed successfully (2959 jobs).
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