Formalization “is a new paradigm for mathematical proof writing

False. Formalization is older than computers and has always been part of math/CS since computers were invented.

Look at how chopped up that quote is. Major tell.

to build a digital library of all of mathematics

False. At best they’ll build a library of all known and formalized mathematics.

the explosion in artificial intelligence has propelled efforts,

False. There is no such thing as “AI”. No reasonable person actually thinks that these programs are “intelligent” any more than a calculator. It’s literally just a computer computing. Current advancements are simply the progression of ancient research plus a completely reasonable and expected increase in computational power.

In theory, such systems may ultimately be able to do things that humans can’t.

Cool theory. In reality these “systems” (ie. computers) have loooong been able to do things that humans can’t. For example, check out a calculator sometime.

one that troubles many mathematicians

False. This is nothing new to mathematicians and many other people. The reality is that people in academia are much more concerned with a stable job, a living wage, etc.

That’s part of why these supposed experts are talking so loose about “AI”. It’s much more important to be funded than accurate.

I think in five years, it is very likely that every single young mathematician uses AI

False. There is no “AI”. There will be no “AI” in five years. But ofc young mathematicians will continue to use computers for a variety of purposes as they always have.