290 Formalization

Nick Andersen, Carter Hastings, Drew Morris, Cameron Briggs, and Matthew Ward

0.1 Test

Definition 1 Even
✓
#

Lean declarations

We say that a number is Even if and only if it is even.

Theorem 2
✓
#

Uses

Lean declarations

Four is Even.

Proof ▶
\[ 4 = 2 \cdot 2. \]