The fact that a piece of software compiles does not necessarily mean that it is correct. The same applies to Lean; in fact, some type theorists are not particularly satisfied with the current state of Lean or the direction in which it is heading.

Mathematician, but not my area. I'd do the same.

Probably the 7/8 has more tricks and special cases to get the better bound. Also, to make the English version close to the Lean version it probably expands some details. So it's longer.

The idea is to understand the 11/12 version, add a few intermediate steps, and get an intuitive understanding of it. Then in a second step go for the 7/8 paper, hopping it's an extension of the 11/12 paper.

Then try to guess 5/6, perhaps as centaur math...

I kinda hate the hard statement that AI "proved" something, when no expert human actually had a chance to look and digest properly the so-called "proof". IMO this whole proof-dump looks like a publicity stunt; just imagine that you have access to a very potent tool, and you strongly believe that it is capable of tackling problems of QRH level, why would you dump hundreds of hard proofs targeted at different areas, rather than focusing on a couple of problems, verifying the bits on the go with experts? It is almost like a company that was caught doing loud yet somewhat empty statements previously, once again is trying to hit the biggest PR coverage rather than trying to cooperate with mathematicians to actually solve those problems.