You · Theoretical computer science · 31 JUL 2026

A manuscript produced by an AI model, released on 1 August 2026 with nine others, gives a direct deterministic reduction from 3SAT that it says proves NP-hardness of approximating the Euclidean closest vector problem to within a factor of n to the power 1/400, with related consequences for the binary nearest codeword problem, at a factor of n to the power 1/200, and for other lattice norms. A Lean certificate accompanies the principal theorem, and the manuscript was prepared by people with the model's help.

Feynman

Insufficient: none of the reduction's steps is available to check, the packet records polynomial-gap hardness of this kind as an open goal, and the Lean statement that could settle most of the claims has not been seen.

06 claims / 09 objections / 10 of 13 sources cited / lenses: Operational test, Formal model, Signal and noise

010203040506OPERATIONAL TESTNo step is identified that turns 3SAT into a polynomial gapA code or gadget shown only to exist is not a procedureA kernel check certifies the formal statement, and Lean has no clockFORMAL MODELSoundness must beat every integer coefficient vector, not only honest assignmentsProducts keep the gap exponent fixed and cannot create oneSIGNAL AND NOISESquared distance equals Hamming distance only for a binary code plus 2Z^nIn the maximum norm the codeword route keeps no gap

Each square is an objection. Larger means heavier. Every claim was challenged by at least one lens.

  1. 01Given any 3SAT formula, the reduction outputs a Euclidean closest vector instance (lattice basis of dimension n, target t, threshold d) such that a satisfiable formula yields a lattice vector within distance d of t, while an unsatisfiable formula leaves every lattice vector farther than n^(1/400) times d from t, including integer combinations of the basis with large, non-Boolean or cancelling coefficients that decode to no assignment.
  2. 02The reduction is deterministic and runs in time polynomial in the formula size, with every code, gadget, composition or amplification step explicit and with polynomial dimension and polynomial bit length of entries, so the conclusion is NP-hardness under a deterministic polynomial-time reduction, not a randomised, quasi-polynomial or conditional one.
  3. 03The gap is strictly polynomial in the final output: with n taken as the dimension of the output lattice rather than the size of the input formula, tracking dimension and gap through every step leaves an exponent of at least 1/400 for all sufficiently large instances, so the growth in dimension never outruns the growth in gap.
  4. 04The binary nearest codeword problem is NP-hard to approximate within n^(1/200), with n the same parameter. The doubled exponent is consistent with squared Euclidean distance equalling Hamming distance, but that identity needs the lattice to be a binary code plus twice the integer lattice, with a binary target; for any other lattice the codeword result needs its own soundness proof.
  5. 05The hardness extends to other lattice norms at polynomial factors, through a transfer that stays deterministic and polynomial-time, with the exponent recomputed for each norm and any increase in dimension from changing norm charged against the gap.
  6. 06The accompanying Lean certificate proves the principal theorem as stated: its formal statement covers the Euclidean lattice distance, the factor n^(1/400), the quantifiers on n, and polynomial-time deterministic computability of the reduction, with no unproved placeholder, added axiom or definition weaker than the informal one. A certificate of only the combinatorial gap would leave the NP-hardness claim unverified.

These are real reviews of public research. Sending your own, and asking follow-up questions, opens with membership.