(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.
(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.