[elias_t]

I wonder if at some point mathematicians will be over-flooded with proofs to check and eventually some over confident false claim will make it into math.

Maybe in the future the work of Mathematicians will be like the ones of SWEs with AI, check thousands of lines of AI generated proof and find the subtle errors

[ykonstant]

>I wonder if at some point mathematicians will be over-flooded with proofs to check and eventually some over confident false claim will make it into math.

That point had come some time ago. Nowadays the literature is both enormous and littered with false proofs and an unknown, but nonzero, number of false published results.

[inigyou]

There are projects to take the entirety of humanity's mathematical knowledge and pour it into a proof checker.

[elias_t]

Do you have the names of such projects?

[YoshiRulz]

From the article: https://mathlib.org

Also https://1000-plus.github.io and https://us.metamath.org

[hiddencost]

That's why the author refused to read a proof from someone he knew until it was formalized in Lean.

[elias_t]

Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?

[Jweb_Guru]

Because you literally don't have to actually understand the proofs, just the definitions and proposition chain. Most of the code is going to be proving auxiliary lemmas or building up internal definitions that aren't needed to understand the final proposition. Then all you have to do is make sure the proof doesn't use any axioms and you're good. Being able to confidently do this is why proof assistants like Lean are really not just another programming language.

(That's not to say there's no value to making the proof themselves nicer--compilation time and reusability can actually be a really big deal in formalized mathematics!--but it's way less important than it is in software).