Lean 4 formalization of First Proof Second Batch Problem 6: an irreducible vertex in a positive-definite integer-weighted tree lattice.
graph-theory formalization mathlib quadratic-forms lean4 lattice-theory first-proof lean-constellation
-
Updated
Aug 7, 2026 - Lean