alt Hacker NewsLean does not reduce the mathematical search space as you suggest. Yes there is a fixed, compact low-level logical core that everything above it depends on. But this is equivalent to an encoding of the logical foundations that mathematics, that formal mathematics depends on in any case. On top that you have mathematical theories built on assumptions (axioms) and you can specify whatever axioms you like and change them at will. To use your analogy: the "search space" is parameterised by user-defined sets of axioms and assumptions.
Could one possibly use Lean to make up their own mathematical model that is wrong but mostly holds up for a while? Kind of like a Sudoku where it’s all working and then you realize one thing doesn’t work so the rest has to be torn down.
I have young kids, and in exploring why boats float I suggested the four elements model. They tested it with bottles full of air and water and earth and it all kind of held up until they found a bowl that floats. Making a wrong model helped the learning process more than telling them the right model. I loved every minute of the science.