A minimal example Lean 4 project demonstrating basic project structure, theorem definitions, proofs, imports, and testing with Lake and Mathlib.