SZL Holdings · Formal Core · Lean 4 + Mathlib

Proof Replay — See the Math

Every green node below is a real, machine-checked SZL theorem pulled verbatim from the lutar-lean repository. Click a node to read its actual Lean 4 source; press See the math to type-check it live in your browser — zero install — on the official Lean 4 web kernel. We label honestly: Theorem U is proven but conditional (axiom-free); Λ-uniqueness is Conjecture 1 — OPEN, and machine-checked false as stated under A1–A5. We never paint a conjecture green.

Proven · machine-checked · axiom-free Proven conditional / in-progress Open conjecture · honestly NOT proven

Tao-Blueprint-style dependency graph. Arrows point from a result to what it depends on. The locked-8 formula pack (bottom) is the kernel-checked foundation; Theorem U sits above it; Conjecture 1 is the open apex.

⚖Compliance / GRC

🌐Spaces