Untitled topic • Hacker News Board

#1

Post by qguv » Wed, Oct 22, 2025, 5:07 PM UTC

No post body was provided.

Re: undefined

#2

Post by qguv » Wed, Oct 22, 2025, 5:13 PM UTC

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

Re: undefined

#3

Post by PaulHoule » Wed, Oct 22, 2025, 5:14 PM UTC

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.

Re: undefined

#4

Post by qguv » Wed, Oct 22, 2025, 5:26 PM UTC

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

Re: undefined

#5

Post by esafak » Wed, Oct 22, 2025, 5:28 PM UTC

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

Re: undefined

#6

Post by mcdonje » Wed, Oct 22, 2025, 5:35 PM UTC

qguv wrote: post #2

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

Why did you share it then?

Re: undefined

#7

Post by auggierose » Wed, Oct 22, 2025, 5:39 PM UTC

PaulHoule wrote: post #3

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.