Comment by bhouston

I am not a mathematician but are most papers now accompanied by a lean proof?

Is there a central repository of lean proofs shared by mathematicians like an npm repository of JavaScript packages?

Does it all depend on a stupid is-odd package in the end?