Formalizing building-up constructions of self-dual codes through isotropic lines in Lean