Hacker News Reader

Comment by gus_massa | Hacker News Reader

> Verification in Lean 4

Someone posted a P=NP solution last week with a verification in Lean, but after looking it used "sorry" and "axiom".

Is your solution "sorry" and "axiom" free?

At the time I posted this submission, the proof was `sorry` and `axiom` free but had 154 `native_decide`s. The proof is enumeration heavy and so for efficiencies sake, the `native_decide`s were used to speed up proof compilation.

Since the submission here, I've had Claude remove the `native_decide`s and optimize the proof so that it now compiles with the three standard axioms only (`propext`, `Classical.choice` and `Quot.sound`).

I've also submitted it to the Palomar registry, which can be seen at:

  https://palomar-registry.org/entry?id=PALOMAR-2026-11-04-000002&version=1

GitHub repo can be found at:

  https://github.com/zzyzek/R2K2ZZN

along with a web demo:

  https://zzyzek.github.io/R2K2ZZN/demo/

In case it's not clear, two-colour Zig Zag Numberlink on rectangles is a special case of the more general NP-complete problem of arbitrary colour count Zig Zag Numberlink on rectangles. With arbitrary colour count, Zig Zag Numberlink is known NP-complete [0]. It was an open problem whether there were polynomial time algorithms when the colour count was finite.

This result doesn't answer the general question of whether there's a polynomial time algorithm for fixed number of colours for the Zig Zag Numberlink problem but provides a partial answer ("yes") of whether for some fixed colour count there exists a polynomial time algorithm. Namely, when the colour count is two, there exists a polynomial algorithm to determine whether the Zig Zag Numberlink problem is solvable and, if solvable, to provide a solution in polynomial time.

[0] https://arxiv.org/abs/1410.5845

Reply on news.ycombinator.com