I think this is AI generated; the Lean snippet on page 33 is full of LaTeX syntax.

I am inclined to dismiss this kind of thing out of hand but it does have the shape of what a successful proof of P != NP, really an expert has to look over the 104 pages and the code.

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.

Nota bene: their Github link 404s, and there are goofy LaTeX mixed in with their Lean snippets.

Why did you share it then?

Unrelated perhaps, but I thought it was curious that this fellow has three academic appointments.