Comment by hardbass

Nobody is forcing anyone to look at anything. Most human math papers don't even have a formal proof and now people are whining when a company goes beyond and releases formal lean proofs.

Do you disagree with the four color theorems proof? Do you know how much compute was used for that?