An introduction to Lax, written as a Lax submission. Lax is an archive that links natural-language mathematics with Lean formalizations: submissions consist of concepts (a statement in prose paired with a faithful Lean encoding), proofs (Lean code discharging a concept's claim), and optionally the paper itself, annotated with markers that tie its passages to the concepts and proofs. This document walks through all three using the prime numbers as a running example: the definition of a prime, Euclid's theorem that there are infinitely many, and a small proof network in which an odd prime between $n$ and $2n$ is derived from Bertrand's postulate, which is deliberately left open for a follow-up submission to prove.