The more famous the problem, the more reputation matters. There is no shortage of papers claiming to prove P vs. NP in either direction. Nobody is taking them seriously, as everyone has a strong prior that people trying to publish such results are cranks.

Mathematicians need to rethink what is the purpose and value of doing pure mathematical research in the future. Until know, they have mostly valued the creation and systematization of human knowledge. From that perspective, Lean proofs mostly increase confidence in the human knowledge. But they don't contribute directly to it, as a formal proof is unlikely to contain insights that are not present in the human proof.