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

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 ?