There have been claims of complex structures on s6 (or absence of them) quite a few times over the last 15 years. Some by acclaimed mathematicians. There was some discussions on HN a few days ago:
I looks like we are breezing past the point where unassisted humans can understand any of this
We understand the proof (most math from all of history) -> We understand how the proof was made (computer-assisted proofs like the four-color theorem) -> We have to trust the computer's explanation for how the proof was made (some LLM proofs)
for all intents an purposes, the paper as well as the lean repo could be full LLM output with zero human involvement
For the rest you only need to check that the formal problem statement matches the actual problem and the proof is not using extra axioms. That's easy to check manually or with a simple script.
Reading the LLM's 12 MB lean output is a bit like trying to maintain a codebase that has been fully vibe-coded as a single giant file, by hand. Even if it's possible in principle, no one is going to enjoy that.