Presumably with the level of interest in it people have been checking what the theorem definitions are to make sure they align and I would expect Anthropic to be burning a huge number of tokens to rip into the proofs and figure out if any of them are exploiting bugs in the lean kernel etc. at a point it's as close to irrefutable as you can get