A multi-agent search discovers candidate nonadditive quantum codes; a Lean 4 + Mathlib library then certifies their Z-type Knill-Laflamme constraints, cross-checked in Wolfram. Includes a distance-2 catalogue, exact BD16 distance-3 examples, and machine-checked no-go results.