> certain ideas get ossified.

That's fine in math. Math is true or it is not. People who overturn popular conjectures in math get fame, not approbation.

Being able to prove things in something like Lean means that stuff like Mochizuki's work on the abc conjecture could be verified or disproven in spite of its impenetrability. Or, at the very least, it could be tackled piecemeal by legions of students tackling a couple of pages every semester.