Alex Albert's repository contains a Lean 4 formalization of mathematical proofs on intrinsic uniqueness and reconstruction across mathematical presentations, with accompanying paper source files, verification scripts, and comprehensive audits documenting the formalization coverage and axiom dependencies.