alt Hacker NewsYou are conflating:
(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.
Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.
Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.
So add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?