proofs(lean4): promote ET-2 to main — L1 conversion is decidable - #27

Merged

hyperpolymath merged 8 commits into

mainfrom

proofs/lean4-l1-l2

Jul 27, 2026

Commits on Jul 21, 2026

proofs(lean4): mechanize the L1/L2 core — hereditary substitution, grade algebras, hard gates

hyperpolymath
and
claude
committed
ci(proofs): enforce https-only redirects on the elan download (Sonar S6506)

hyperpolymath
and
claude
committed

Commits on Jul 22, 2026

proofs(lean4): close ET-2 — L1 conversion is decidable

hyperpolymath
and
claude
committed
proofs(lean4): close ET-2 — L1 conversion is decidable (#24)
hyperpolymath
authored