Dumb question— why doesn’t proof proposal construction (not the solution) in lean get celebrated more ? That seems central to understanding.

If these proofs are so important why is there not a central repositories of the proposal in a formalized language ?