lean-architect-example

Thomas Zhu

Definition 1
✓
#

Lean declarations

Natural numbers.

Definition 2
✓
#

Uses

Lean declarations

Natural number addition.

Theorem 3
✓
#

Uses

Lean declarations

For any natural number \(a\), \(0 + a = a\), where \(+\) is definition 2.

Proof ▶

The proof follows by induction.

Theorem 4
#

Uses

Lean declarations

For any natural numbers \(a, b\), \((a + 1) + b = (a + b) + 1\).

Proof ▶

Proof by induction on \(b\).

Theorem 5
#

Uses

Lean declarations

For any natural numbers \(a, b\), \(a + b = b + a\).

Proof ▶

The base case follows from theorem 3.

The inductive case follows from theorem 4.

Definition 6
#

Uses

Lean declarations

Natural number multiplication.

Theorem 7
#

Uses

Lean declarations

For any natural numbers \(a, b\), \(a * b = b * a\).

Proof ▶
Theorem 8 Taylor-Wiles
#

Uses

Lean declarations

Discussion

Fermat’s last theorem.

Proof ▶

See [ .