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.