Lean 4 Theorem Proving — Formal Proof Verification

Introduction

AutEng integrates Lean 4 with Mathlib for formal theorem proving. Unlike CAS verification (which uses heuristic symbolic computation), Lean provides machine-checked proofs—if your proof compiles, it's mathematically correct.

Every Lean proof is either verified (✅), has errors (❌), or is pending (🔄). There's no "unknown" state—Lean's type system guarantees correctness.

Quick Start

Wrap your Lean code in a :::lean block. The system will compile and verify it using Lean 4 + Mathlib.

Example 1: Simple Theorem ✅

A basic proof using the omega tactic:

1import Mathlib.Tactic
2
3theorem add_comm_example (a b : ℕ) : a + b = b + a := by
4  omega

Expected Result: ✅ Verified — The proof type-checks successfully.

Example 2: Proof by Induction ✅

A classic result: the sum of the first n odd numbers equals n². This requires induction and the ring tactic.

1import Mathlib.Tactic
2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3
4open Finset BigOperators
5
6theorem sum_odd_numbers (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n^2 := by
7  induction n with
8  | zero => simp
9  | succ n ih =>
10    rw [sum_range_succ, ih]
11    ring

Expected Result: ✅ Verified — The induction proof is complete.

Example 3: Incomplete Proof ❌

Using sorry marks a proof as incomplete. Lean will report this as an error:

1import Mathlib.Tactic
2
3theorem incomplete_example (n : ℕ) : n + 0 = n := by
4  sorry

Expected Result: ❌ Failed — Declaration uses 'sorry'.

Common Tactics

Lean 4 with Mathlib provides powerful tactics for constructing proofs:

Example: Using Multiple Tactics

1import Mathlib.Tactic
2
3-- Sum of first n natural numbers
4theorem sum_naturals (n : ℕ) : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) := by
5  induction n with
6  | zero => simp
7  | succ n ih =>
8    simp [Finset.sum_range_succ]
9    linarith

Common Imports

Mathlib provides a vast library of mathematical definitions and lemmas. Here are the most commonly used imports:

CAS vs Lean: When to Use Each

Both CAS and Lean verify mathematical correctness, but they serve different purposes:

Example Comparison

Verifying sin²x + cos²x = 1:

Proving ∑(2i+1) = n² for all n:

1import Mathlib.Tactic
2import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3
4open Finset BigOperators
5
6theorem sum_odd_eq_square (n : ℕ) : ∑ i ∈ range n, (2 * i + 1) = n^2 := by
7  induction n with
8  | zero => simp
9  | succ n ih => rw [sum_range_succ, ih]; ring

Error Messages

When a proof fails, Lean provides detailed error messages with line numbers and suggestions:

Type Mismatch

1import Mathlib.Tactic
2
3-- This will fail: can't prove n = n + 1
4theorem wrong_claim (n : ℕ) : n = n + 1 := by
5  rfl

Expected Error: type mismatch — rfl requires definitionally equal terms.

Tactic Failed

1import Mathlib.Tactic
2
3-- omega can't prove this (it's false!)
4theorem false_claim (n : ℕ) : n > n := by
5  omega

Expected Error: omega could not prove the goal.

Best Practices

Reference

Block Syntax

Status Indicators

Performance

Next Steps

Ready to explore more verification options? Check out these related guides:

• CAS Verification Demo — Quick algebraic identity checking with SymPy
• Quadratic Formula Derivation — Step-by-step equation solving with CAS
• KaTeX Syntax Reference — Mathematical notation in Markdown