Study pack · AI and computer science

Hardness of the closest vector problem

Theoretical computer science · as it stood on 31 July 2026 · run unseen-2026-11-07/closest-vector-hardness · Claude Opus 5.5

Not enough to judgeNo break

No step is identified that turns 3SAT into a polynomial gap.

claims: 6
holes: 9
lenses: 3
records cited: 10 of 13
retracted precedents: 1

What happened, 9 September 2026. A stronger theorem and a human audit support it. An independent paper proved stronger deterministic bounds: n to the power 1/8 minus epsilon for closest vector, and n to the power 1/4 minus epsilon for nearest codeword, which entail the weaker result if the definitions match. A human audit of the review record, dated 9 September 2026, found no confirmed substantive error and called this the strongest outside corroboration among the ten results, while noting that some threshold and degree calculations remain compressed. Asked first, the model said it didn’t know how it ended.

The idea, as it stood

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.

Given 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.mathematical · unsupported
The 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.mathematical · unsupported
The 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.mathematical · unsupported
The 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.mathematical · unsupported
The 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.mathematical · unsupported
The 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.mathematical · unsupported

The holes, and who found them

More than one lens found a hole in claim 1, each on its own. That is a stronger signal than one lens alone.

#	Hole	Lens	How serious	Claim	Status
1	No step is identified that turns 3SAT into a polynomial gap	Alan Turing	serious	1	Open
2	Soundness must beat every integer coefficient vector, not only honest assignments	John von Neumann	serious	1	Open
3	Products keep the gap exponent fixed and cannot create one	John von Neumann	serious	3	Open
4	A code or gadget shown only to exist is not a procedure	Alan Turing	serious	2	Open
5	Squared distance equals Hamming distance only for a binary code plus 2Z^n	Claude Shannon	serious	4	Open
6	In the maximum norm the codeword route keeps no gap	Claude Shannon	serious	5	Open
7	A kernel check certifies the formal statement, and Lean has no clock	Alan Turing	serious	6	Open
8	The hard codes must have dimension well above n^(1/200) log n	Claude Shannon	minor	4	Open
9	The quantifiers disagree, and no experiment can see a gap this small	Alan Turing	minor	1	Open

What it rests on

Proof verification and the hardness of approximation problemsArora et al. · 1998 · Journal of the ACM · cited on claim 1, 2 · doi:10.1145/278298.278306
An Approach To The Sliding Scale Conjecture Via Parallel Repetition For Low Degree Testing.Moshkovitz · 2014 · Electronic colloquium on computational complexity · cited on claim 1 · record
Approximating SVP∞ to within almost-polynomial factors is NP-hardDinur · 2002 · Theoretical Computer Science · cited on claim 1, 5 · doi:10.1016/s0304-3975(01)00290-0
Deterministic approximation algorithms for the nearest codeword problemAlon et al. · 2010 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · cited on claim 4 · doi:10.4230/dagsemproc.09421.4
Polynomially Low Error PCPs with polyloglog n Queries via Modular CompositionDinur et al. · 2015 · ACM Symposium on Theory of Computing (STOC) · cited on claim 1 · doi:10.1145/2746539.2746630
The Projection Games Conjecture and the hardness of approximation of super-SAT and related problemsMukhopadhyay · 2021 · Journal of Computer and System Sciences · cited on claim 1 · doi:10.1016/j.jcss.2021.09.002
More on average case vs approximation complexityAlekhnovich · 2004 · Annual Symposium on Foundations of Computer Science · cited on claim 4 · doi:10.1109/sfcs.2003.1238204
PCP Characterizations of NP: Toward a Polynomially-Small Error-ProbabilityDinur et al. · 2011 · Computational Complexity · cited on claim 1 · doi:10.1007/s00037-011-0014-4
SETH-Hardness of Coding ProblemsStephens-Davidowitz & Vaikuntanathan · 2019 · Annual Symposium on Foundations of Computer Science · cited on claim 4 · doi:10.1109/focs.2019.00027
Near Optimal Alphabet-Soundness Tradeoff PCPsMinzer & Zheng · 2024 · ACM Symposium on Theory of Computing (STOC) · cited on claim 1 · doi:10.1145/3618260.3649606
Closest Vector ProblemMicciancio & Goldwasser · 2002 · Springer eBooks · retrieved, not cited · doi:10.1007/978-1-4615-0897-7_3
Computation Offloading in Mobile Cloud Computing and Mobile Edge Computing: Survey, Taxonomy, and Open IssuesMaray & Shuja · 2022 · Mobile Information Systems · retracted · retrieved, not cited · doi:10.1155/2022/1121822
Data-Driven Approximations to NP-Hard ProblemsMilan et al. · 2017 · Proceedings of the AAAI Conference on Artificial Intelligence · retrieved, not cited · doi:10.1609/aaai.v31i1.10750

The tests that settle it

The deciding test · days of work

Audit the Lean certificate against the informal theorem. Compile it, run #print axioms on the principal theorem, list every hypothesis it takes, and read the statement and each definition it relies on. It should say that, for all sufficiently large instances, the reduction sends satisfiable formulas to instances with a lattice vector within d of t and unsatisfiable ones to instances where every integer combination of the basis, coefficients ranging over all of Z^m, lies farther than n^(1/400) d from t in the Euclidean norm, with n the output dimension, and it should give the reduction as a computable function with a polynomial running-time bound in an explicit machine model.

It fails if: The principal theorem depends on sorryAx or an added axiom; takes the gap source (a code, gadget or PCP with the needed parameters, or a conjecture) as a hypothesis; restricts coefficients to Boolean or bounded values; measures n as the formula size; or proves a factor below n^(1/400). If only the running-time clause is missing, C6 fails as stated and the NP-hardness claim falls back on an unchecked prose argument.

For hole	Test	Result
1	Find the lemma where the ratio between the unsatisfiable and satisfiable distances first exceeds a constant, write that ratio (or the underlying soundness error) as an explicit function of the input size N, and check that it is at least N^a for a fixed a > 0 with a complete, unconditional proof. Counts against the claim: the gap source is a conjecture such as the Sliding Scale or Projection Games Conjecture, enters as a hypothesis, or grows only as N^(o(1)), for example 2^(log N / log log N).	Proposed
2	Confirm that the soundness lemma's hypothesis ranges over all z in Z^m. Then, on the variable and clause gadgets and on the smallest full instances the construction allows, search all coefficient vectors with entries in [-3, 3] and, where the dimension permits, solve the closest vector problem exactly for small unsatisfiable formulas such as the eight clauses on three variables. Counts against the claim: the lemma assumes coefficients in {0, 1} or a bounded range, or any unsatisfiable instance has a lattice vector within n^(1/400) d of t.	Proposed
3	Tabulate, for every step, the dimension, gap, entry bit length and running time as explicit functions of N, and compute the limit of log(gap)/log(dimension) on the final output. Counts against the claim: the limit is below 1/400 or is 0, any step's dimension is super-polynomial in N, or an amplification lemma bounds only product vectors.	Proposed
4	For each code and gadget, identify the algorithm that builds it, its running time and the bit length of its entries, and flag any object drawn at random, found by search over a super-polynomial space, or defined only by an existence argument. Counts against the claim: such an object is used and no explicit deterministic construction with the required parameters is given.	Proposed
5	Check whether the output lattice contains 2Z^n, whether its image mod 2 is a binary linear code, and whether t is a 0/1 vector. Counts against the claim: the lattice is not of this form and the manuscript gives no separate codeword reduction with its own soundness proof.	Proposed
6	For each norm claimed, write the transfer map, its distortion D and output dimension m as functions of n, and compute log(g/D)/log m. Counts against the claim: the maximum-norm result rests on the codeword identity, a transfer map is chosen at random, or the recomputed exponent is not positive.	Proposed
7	Compile the development, run #print axioms on the principal theorem (propext, Classical.choice and Quot.sound are acceptable; sorryAx or Lean.ofReduceBool are not), search for sorry, admit, axiom and opaque declarations, check that the reduction is not marked noncomputable, and read the statement and each definition it uses against the four points. Counts against the claim: any point fails.	Proposed
8	Compute the dimension k and block length n of the output codes as functions of N. Counts against the claim: k = o(n^(1/200) log n) on the instances used for hardness.	Proposed
9	Read the quantifier on n in the manuscript's theorem and in the formal statement. Counts against the claim: the gap is proved only for some n, or only for special sizes the reduction cannot always reach.	Proposed

Proposed tests that haven’t run are the agenda for what comes next. Download them as a draft pre-registration, ready to edit and register on OSF.

Two answers, matched blind

The same model answered twice: once plainly, as a standard AI, and once through Feynman. Both answers’ findings were matched blind, without the ending.

The lenses found, the standard AI missed

Soundness must beat every integer coefficient vector, not only honest assignments Von Neumann's minimax and his question about available strategies led the lens to read soundness as a game: an adversary picks any integer vector, so non-Boolean choices must be priced. It cites nothing; the lens supplies the worst-case reading, as NP-hardness postdates it. The standard AI’s soundness point concerned surviving cheap local repairs instead.

Products keep the gap exponent fixed and cannot create one Von Neumann's 'reliable wholes from unreliable parts' led the lens to warn that multiplying soundness bounds assumes the cheating vector factors, as redundancy assumes independent failures; his question about each move's consequences fits its demand for an exponent ledger. It cites nothing. The standard AI instead weighed the factor against the long-standing n^(c/log log n) barrier.

A code or gadget shown only to exist is not a procedure Turing's 'limits of any procedure' led the lens to require one definite mechanical procedure, treating codes or gadgets shown only to exist as randomised or non-uniform steps. The cited 1998 paper, postdating the lens, added that O(log N) random bits can be enumerated away, poly(N) cannot. The standard AI found determinism unsurprising, the earlier reduction being deterministic too.

Squared distance equals Hamming distance only for a binary code plus 2Z^n Shannon's question of which distinctions survive transmission led the lens to ask whether the Euclidean gap survives translation into Hamming distance, arguing it does only for a binary code plus 2Z^n. The cited 2004 and 2019 papers, postdating the lens, give only conditional nearest-codeword hardness. The standard AI instead called the three results really one.

The hard codes must have dimension well above n^(1/200) log n Shannon's 'information as resolved uncertainty' led the lens to treat the 2^k codewords as uncertainty a decoder must resolve, and to require enough of it to outpace known algorithms. The cited 2010 paper, postdating the lens, reported those O(k/c) and O(k/log n) algorithms. The standard AI instead noted the factor sits far below the square root of n.

The standard AI found, the lenses missed

It would break a long-standing barrier The standard AI drew on the record it cited: Dinur, Kindler, Raz and Safra's n^(c/log log n) factor, the open sliding scale conjecture and low-error PCPs, concluding a low prior, not a contradiction. Feynman’s lenses examined the reduction instead: no step is identified that turns 3SAT into a polynomial gap, and products cannot create one.

Ten manuscripts and no independent check reported The standard AI drew on the description: a model and helpers but no named checker, no outside review or publication, and ten manuscripts released together, adding that central results take months of expert reading. Feynman’s lenses instead examined the certificate: a kernel check certifies the formal statement, and Lean has no clock.

The finding

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.

It held up: A stronger theorem and a human audit support it. What would overturn the review’s reading: The principal theorem depends on sorryAx or an added axiom; takes the gap source (a code, gadget or PCP with the needed parameters, or a conjecture) as a hypothesis; restricts coefficients to Boolean or bounded values; measures n as the formula size; or proves a factor below n^(1/400). If only the running-time clause is missing, C6 fails as stated and the NP-hardness claim falls back on an unchecked prose argument.

Cite it, disclose it, reproduce it

A paragraph for your methods section

We used Feynman (feynman.works), an AI research-review tool running on Claude Opus 5.5, to critique “Hardness of the closest vector problem” on 2026-11-07 (run unseen-2026-11-07/closest-vector-hardness). It reconstructed 6 claims, retrieved 13 published records dated no later than 2026-07-31, and raised 9 objections through reasoning frameworks drawn from the published work of Alan Turing, John von Neumann and Claude Shannon. Each citation in its output was checked against the records it retrieved, and we read every source we relied on. Its objections informed our analysis; the conclusions, and any errors, are our own.

The lenses

Alan TuringComputation & intelligence · 1936–1954What observable test would let us distinguish the competing claims?
John von NeumannMathematics & strategy · 1928–1957What are the incentives, available strategies and consequences of each move?
Claude ShannonInformation theory · 1937–1961Which distinctions survive transmission, and which are lost?

BibTeX

@misc{feynman-unseen-2026-11-07-closest-vector-hardness,
  title = {{Feynman review: Hardness of the closest vector problem}},
  author = {{Feynman Works}},
  year = {2026},
  howpublished = {\url{https://www.feynman.works/pack/closest-vector-hardness}},
  note = {Run unseen-2026-11-07/closest-vector-hardness, Claude Opus 5.5, 2026-11-07}
}

@article{arora1998proof,
  title = {{Proof verification and the hardness of approximation problems}},
  author = {Arora and others},
  year = {1998},
  journal = {Journal of the ACM},
  doi = {10.1145/278298.278306}
}

@article{moshkovitz2014approach,
  title = {{An Approach To The Sliding Scale Conjecture Via Parallel Repetition For Low Degree Testing.}},
  author = {Moshkovitz},
  year = {2014},
  journal = {Electronic colloquium on computational complexity},
  url = {https://dblp.uni-trier.de/db/journals/eccc/eccc21.html#Moshkovitz14}
}

@article{dinur2002approximating,
  title = {{Approximating SVP∞ to within almost-polynomial factors is NP-hard}},
  author = {Dinur},
  year = {2002},
  journal = {Theoretical Computer Science},
  doi = {10.1016/s0304-3975(01)00290-0}
}

@article{alon2010deterministic,
  title = {{Deterministic approximation algorithms for the nearest codeword problem}},
  author = {Alon and others},
  year = {2010},
  journal = {DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)},
  doi = {10.4230/dagsemproc.09421.4}
}

@article{dinur2015polynomially,
  title = {{Polynomially Low Error PCPs with polyloglog n Queries via Modular Composition}},
  author = {Dinur and others},
  year = {2015},
  journal = {ACM Symposium on Theory of Computing (STOC)},
  doi = {10.1145/2746539.2746630}
}

@article{mukhopadhyay2021projection,
  title = {{The Projection Games Conjecture and the hardness of approximation of super-SAT and related problems}},
  author = {Mukhopadhyay},
  year = {2021},
  journal = {Journal of Computer and System Sciences},
  doi = {10.1016/j.jcss.2021.09.002}
}

@article{alekhnovich2004more,
  title = {{More on average case vs approximation complexity}},
  author = {Alekhnovich},
  year = {2004},
  journal = {Annual Symposium on Foundations of Computer Science},
  doi = {10.1109/sfcs.2003.1238204}
}

@article{dinur2011pcp,
  title = {{PCP Characterizations of NP: Toward a Polynomially-Small Error-Probability}},
  author = {Dinur and others},
  year = {2011},
  journal = {Computational Complexity},
  doi = {10.1007/s00037-011-0014-4}
}

@article{stephens2019seth,
  title = {{SETH-Hardness of Coding Problems}},
  author = {Stephens-Davidowitz and Vaikuntanathan},
  year = {2019},
  journal = {Annual Symposium on Foundations of Computer Science},
  doi = {10.1109/focs.2019.00027}
}

@article{minzer2024near,
  title = {{Near Optimal Alphabet-Soundness Tradeoff PCPs}},
  author = {Minzer and Zheng},
  year = {2024},
  journal = {ACM Symposium on Theory of Computing (STOC)},
  doi = {10.1145/3618260.3649606}
}

Run unseen-2026-11-07/closest-vector-hardness on Claude Opus 5.5. The review is reproducible from its record: the claims, the records retrieved before 31 July 2026, and each lens’s card. https://www.feynman.works/pack/closest-vector-hardness