The recent proof of Fermats Last Theorem is interesting: it is (iirc) 13 million lines of lean code. And type-checking takes 5 hours or so on a pretty beefy machine. I cannot independently verify the proof, and I have to take Anthropics word for it that it actually type-checks.
It'd cost you $30-$50 on AWS for a clean Lean build or maybe $100-$150 for the full verification suite. You are, in fact, capable of independently verifying the proof yourself if you don't trust all the people who've already done so.
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.
With human proofs, I have some trust in process behind it.