Simple symmetric Venn diagrams with 17 and 19 curves: certificates, checkers, Lean verifications and paper

Simple, rotationally symmetric Venn diagrams with 17 curves and with 19 curves, the first beyond the 13-curve diagrams of Mamakani and Ruskey (2014), given as machine-checkable certificates, together with an independent checker, formal verifications in Lean 4 of one certificate of each size, the search code that found them, a plotter, renderings, and the write-up. Version 1.2 (2026-09-22) adds three 19-curve certificates found by runs started fresh from the resolved Griggs–Killian–Savage diagram (one of them with the plain recipe and no unlocking proposal), the check that all nine 19-curve certificates are pairwise non-isomorphic, and the paper as submitted to arXiv. Version 1.1 remains available under its own DOI. Contents of venn17-1.2-source.zip (snapshot of the repository github.com/dzoba/venn17 at commit 5f689d9, version 1.2, 2026-09-22): certificates/: fifteen certificates with SHA256SUMS: four 17-curve (venn17-local-c3-s2, venn17-gcp-s12, venn17-gcp-s14, venn17-gcp-s16), nine 19-curve (venn19-closure-s196002, s196004, s195001, s196001, s196007, s195002 from the closure runs; venn19-fresh-s192015, venn19-fresh-s190002, venn19-fresh-s192007 from fresh starts), and one 11-curve and one 13-curve non-monotone example. Each certificate lists the 2^n - 2 crossings as quadruples of n-bit region labels. verify/verify.py: standalone checker (Python, NumPy); verify/RESULTS.md and verify/RESULTS-19.md are its transcripts on all fifteen files. verify/monotone_test.py: Bultena-Grunbaum-Ruskey monotonicity test. verify/lean/: Justin Grimes's independent Lean 4 formalization proving that certificate venn17-local-c3-s2 is a simple rotationally symmetric 17-Venn diagram (Apache-2.0, his LICENSE and CITATION preserved). verify/lean19/: the port of that formalization to 19 curves, proving the same statement for venn19-closure-s196002 (same axiom list: propext, Classical.choice, Quot.sound and twenty native_decide certificates). search/: the relaxed Metropolis walk (relaxed_walk5.cpp) and the run configurations that produced the diagrams. plotter/, images/: the plotter and renderings. paper/venn17-19.pdf, .tex: the write-up as submitted to arXiv on 2026-09-22 (math.CO; identifier to be added here once assigned). venn19-lean-proof.zip is the standalone Lean 19 package (identical to verify/lean19/ in the source zip). venn17-19.pdf is the paper. certificates-SHA256SUMS.txt lists the SHA-256 of every certificate. UPLOADS-SHA256.txt lists the SHA-256 of the other files in this record. Verification: unzip, then python3 verify/verify.py certificates/<file>.json (seconds for 17, about a minute for 19). The Lean developments rebuild with the pinned toolchain (lean-toolchain, lake-manifest.json); see their README files. The search was designed and carried out by AI systems (Claude, Anthropic; Codex, OpenAI) under the direction of Chris Dzoba; the paper states their roles in full. The certificates stand on their own: nothing about their validity depends on how they were produced.