I've been following the story. Git repos of Lean code are a good start to developing understanding. First verify that the proof is correct, then work on ways to simplify it and make it understandable.
The issue is that the auto-formalization step itself is not trivial. There is no formal verification which proves the translation correct, so it is up to mathematicians to hand-check the formalization to make sure it’s saying the same thing. Unfortunately, this problem is undecidable in general.
We’ve already had a paper showing that auto-formalization can’t be trusted implicitly [1], so a GitHub repo of a bunch of Lean code can’t be trusted to prove what the title claims is being proved.