Comment by Silamoth

Did you read TFA? They never claimed they’ve formalized all of mathematics. For a couple decades now, mathematicians have been discussing formalizing all of mathematics. Some are now proposing AI can be used for this. But TFA argues that’s not necessarily the best approach. It’s a discussion of how to move forward in formalizing all of math, not a claim about having done so. Not clickbait at all.