Well, isn't the idea just to run the Lean proof and be sure? No need to read the 104 pages after ensuring that the statement in Lean actually means P != NP.
If that is not possible in less than an hour (plus the Lean running time), then Lean is not fit for purpose yet.