Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two

Verification with Lean is a piece of empirical evidence that the proof is correct. The paper passing peer review would be another. But even together, those two would be insufficient to establish the claim. While it's a convenient to assume that mathematics deals with logical statements, any attempt to evaluate those statements relies on physical processes with both known and unknown failure modes. There cannot be a test that establishes it unambiguously whether a claim is true or false. In all nontrivial situations, mathematical truth is based on expert consensus. When a new claim is made, people will try to raise and resolve objections, until a consensus emerges one way or another. As for C++, all compilers are different. For any given compiler, there are valid C++ programs the compiler fails to compile and invalid programs it compiles without any errors or warnings. And now that I think of it, a new version of a compiler crashing with valid code earlier versions used to handle is the only class of compiler bugs I see with any regularity.