PaulHoule
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.
auggierose
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.
qguv
Nota bene: their Github link 404s, and there are goofy LaTeX mixed in with their Lean snippets.
mcdonje
Why did you share it then?
esafak
Unrelated perhaps, but I thought it was curious that this fellow has three academic appointments.
I think this is AI generated; the Lean snippet on page 33 is full of LaTeX syntax.