The Purpose of Proofs

In discussions of AI and Mathematics, the discussion often goes to mathematical proofs, such as the the First Proof challenge. So let's look at the role of proofs in mathematics.

Without a proof, you don't even know whether a theorem is true or false. It's not even a theorem until you have a proof, just a conjecture or hypothesis. You might have some intuition but you don't know the hardness of a proof until you find it. Even then that only gives you an upper bound on hardness as someone might find a simpler alternative proof in the future,

Proofs give an understanding of why a theorem is true. A proof can look like a piece of art, especially if the proof works in a new or clever way, maybe even a proof from the book like Kelly's Proof of the Sylvester–Gallai theorem. A mathematician often has their most satisfying experiences finding a proof of a theorem they or others have had challenge proving earlier.

Conjectures drive the need for proofs, but often it goes the other direction. A failed proof leads to a new conjecture and maybe a different theorem altogether. My time-space tradeoffs came out of a failed attempt to show NP different from L. Too often I see papers with theorems that are really just what the best proof they can find achieves.

Proofs are supposedly objective, either it is a valid proof or it isn't, the biggest reason AI tackles proofs as we can grade them as right or wrong. Most academic papers have high-level proofs and a referee however needs to make a subjective decision whether the proof has enough details to count as a legitimate proofs. If a proof has minor fixable errors, then it isn't a proof but we usually count it as one.

Now we have proof systems like Lean where we can make proofs truly objective. There's a large mathlib project to formalize much of mathematics in Lean, and talk of a cslib as well. 

Lean excites me less, I'm not sure what we gain by formalizing proofs besides certainty. Will Fermat's last theorem be any more true once we formalize it? One could argue Lean also helps AI reason about mathematics in a grounded way, though could AI just get lost in the logical weeds?

I worry about the heavy task of converting proofs to Lean, even with AI help, takes away from time spent finding and proving new theorems and we lose the beauty of the proofs. If there was a fully lean verified proof of P ≠ NP that you couldn't understand, would you find that satisfying?