Import GapCVP hardness formalization - #396
Conversation
Greptile SummaryThe PR imports and registers the GapCVP hardness formalization as a chain of incremental Lean modules.
|
| Filename | Overview |
|---|---|
| LeanPool/GapCVP/Part01A.lean | Introduces the foundational problem definitions, encodings, reductions, and shared machine-proof infrastructure used throughout the formalization. |
| LeanPool/GapCVP/Part18.lean | Exposes the four advertised NP-hardness endpoints, whose formal types align with the catalog claims examined during this review. |
| LeanPool/GapCVP.lean | Defines the project entry module by importing the terminal module in the complete linear dependency chain. |
| LeanPool.lean | Adds every GapCVP module to the repository-wide aggregate import list. |
| LeanPool/projects.yml | Registers the GapCVP project, its four main results, source revision, license, authors, and mixed provenance. |
Reviews (4): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 31,314 maxHeartbeats units across 69 files (136,795 added LOC). Sum of Count-heartbeats wall-clock total: 760.03 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.GapCVP.Part09 |
26.00 s |
LeanPool.GapCVP.Part13 |
25.00 s |
LeanPool.GapCVP.Part01A |
20.00 s |
LeanPool.GapCVP.Part14B |
19.00 s |
LeanPool.GapCVP.Part12C |
17.00 s |
LeanPool.GapCVP.Part15 |
13.00 s |
LeanPool.GapCVP.Part10A |
12.00 s |
LeanPool.GapCVP.Part08D |
11.00 s |
LeanPool.GapCVP.Part16A |
11.00 s |
LeanPool.GapCVP.Part02 |
10.00 s |
LeanPool.GapCVP.Part03C |
10.00 s |
LeanPool.GapCVP.Part07D |
10.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 69 files; the per-file table shows only the 69 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | 🤔 discuss |
The card and all four claimed endpoint statements are elided, so their quantifiers, hypotheses, and conclusions cannot be audited for faithfulness. |
| Novelty | ✅ pass |
The prior-art searches ran for all four headlines and found no Mathlib or pooled declaration proving any of them. |
| Significance | ✅ pass |
This is research-level theory building around a named hardness result for approximate closest vector. |
| Sources | ✅ pass |
The identified upstream formalizations are credited, but the cited repository’s support for the claimed hardness endpoints is unverifiable from the partial diff. |
| Code quality (advisory) | 🤔 discuss |
The simulation code is competent, but the comparator and statement-lifting paths duplicate enough proof infrastructure that a maintainer should decide whether to require another abstraction pass. |
| Aspect | Value |
|---|---|
| Proves the claim | ➖ unverifiable |
| Assumed, not proved | Unverifiable: the headline theorem statements and the card summaries that would disclose bundled hypotheses are both omitted. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | lattice complexity |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The visible Lean contains supporting constructions, while the statements of gapCVP400IsNPHard, binaryNearestCodewordIsNPHard, binarySyndromeDecodingIsNPHard, and finitePNormGapCVPIsNPHard are absent.
The Lean develops polynomial-time Turing-machine, tableau, and CNF-reduction infrastructure toward GapCVP.Comparator.gapCVP400IsNPHard, a substantive result in lattice-based computational complexity.
Faithfulness findings (1)
- elided-headline —
LeanPool/GapCVP/Part18.lean
Provide the card and the complete Lean statements of all headline declarations; without them, this review cannot compare the claimed NP-hardness results against their formal quantifiers, approximation regimes, reductions, or assumed inputs.
Evidence: prose only
Code quality findings (2)
- duplicate-proof-structure — PR-wide
Part03G and Part04B separately implement the same malformed length-prefixed-input case tree: missing first record, truncated first record, missing second record, truncated second record, and the total dispatcher. The trace composition and budget arguments are correspondingly parallel. Extend the existingDelimitedCompareTraceabstraction to cover these malformed branches, parameterized by the comparator step and output semantics, so parser or phase changes do not require synchronized edits to both families.
Evidence: InLeanPool/GapCVP/Part03G.lean,delimitedCompare_totalTracecontains:
cases unaryInputSplit input with | inl witness => obtain ⟨count, hinput⟩ := witness subst input exact delimitedCompare_missingFirstTrace count
In LeanPool/GapCVP/Part04B.lean, certifiedNatural_totalTrace repeats the dispatcher as:
cases unaryInputSplit input with | inl witness => obtain ⟨count, hinput⟩ := witness subst input exact certifiedNatural_missingFirstTrace count
The two files also separately declare delimitedCompare_truncatedFirstTrace, delimitedCompare_missingSecondTrace, delimitedCompare_truncatedSecondTrace and their certifiedNatural_ counterparts.
- duplicate-definition — PR-wide
The PR defines several independent recursive embeddings ofTuring.TM2.Stmt, followed by parallel constructor-by-constructor simulation proofs. A reusable statement homomorphism parameterized by stack and label embeddings, state projection, and halt continuation would centralize this machinery. As written, changes to the statement language require synchronized updates toliftValidStatement,liftBoundedFoldWorkerStatement,liftFormulaPreservationCanonicalStmt, andliftOriginalSourcePreservingStatement, together with theirstepAuxproofs.
Evidence:LeanPool/GapCVP/Part04D.leancontains:
private def liftBoundedFoldWorkerStatement (tm : Turing.FinTM2) : Turing.TM2.Stmt tm.Γ tm.Λ tm.σ → Turing.TM2.Stmt (boundedFoldAlphabet tm) (BoundedFoldLabel tm) (BoundedFoldState tm) | .push k f next => .push (.inl k) (fun state => f state.2) (liftBoundedFoldWorkerStatement tm next)
LeanPool/GapCVP/Part05D.lean repeats the same traversal pattern:
private def liftOriginalSourcePreservingStatement (tm : Turing.FinTM2) : Turing.TM2.Stmt tm.Γ tm.Λ tm.σ → Turing.TM2.Stmt (originalSourcePreservingAlphabet tm) (OriginalSourcePreservingLabel tm) (OriginalSourcePreservingState tm) | .push stack value next => .push (.inl stack) (fun state => value state.2) (liftOriginalSourcePreservingStatement tm next)
The corresponding proofs are independently declared as liftBoundedFoldWorkerStatement_stepAux and liftOriginalSourcePreservingStatement_stepAux; the same file set also contains liftValidStatement_stepAux and liftFormulaPreservationCanonicalStmt_stepAux.
Tokens: 1,180,466 in / 14,954 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $3.1755
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
|
Addressed every code-quality finding at
The same pass also factored the 87%-similar exact/finite-p physical-routing case split through one narrowly scoped helper. Overall this review commit is 1,171 additions / 2,052 deletions (net -881 physical lines and -899 non-comment code lines). It replaces 25 declarations with 25 shared declarations, and the refreshed source+kernel closure finds all 8,019 project declarations reachable from the four endpoints (dead: 0). For the faithfulness concern, Exact-head verification is green: true clean 3,221-job build, aggregate collision compile, full quality audit, |
# Conflicts: # LeanPool/projects.yml
Automation disposition: needs-maintainerReviewed exact head |
Vilin97
added
the
needs-maintainer
1 participant
Summary
Imports the GapCVP development from OpenAI's
ten-proofsat canonical commit94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6. The port proves four headlineNP-hardness results for approximate closest vector, binary nearest codeword,
binary syndrome decoding, and finite p-norm GapCVP.
The canonical four
GapCVP.Comparatorstatement chunks are preserved exactly:gapCVP400IsNPHardbinaryNearestCodewordIsNPHardbinarySyndromeDecodingIsNPHardfinitePNormGapCVPIsNPHardThis also incorporates implementation and proof refactorings from Dean Cureton's
optimized fork at commit
30c21d72a2ee3308d66c945387729d736e0cb305, so theproject is registered with
mixprovenance and both authors are credited.Optimization and audit
Mathlibimport with a measured narrow frontier. Thetarget graph falls from 8,724 to 3,221 jobs (63.1%).
largest module 8,115 non-comment code lines, largest proof block 190 lines.
initial port: kernel-visible declarations fall from 8,046 to 8,019; source
declaration commands fall from 8,029 to 8,009.
abstractions while deleting 881 physical / 899 non-comment code lines. It
factors 14 repeated failure-trace recursions, the non-comparison phases of
the two comparator machines, and the exact/finite-p physical-routing split.
changes: 8,019 / 8,019 declarations reachable, zero dead nodes.
for private-name leakage; the small shared API is consumed across modules.
complexity abstractions. None had genuinely matching interfaces, so this adds
no cross-project dependency.
Canonical source size is 130,430 physical / 120,836 non-comment code lines. The
fully compliant and review-optimized port is 135,914 physical / 122,598
non-comment code lines; the increase is the required per-file
headers/documentation, 100-column formatting, and honest continuation-module
scaffolding. The declaration counts above capture the semantic DCE independently
of that formatting overhead.
The canonical monolith does not compile on the pool's Lean 4.34 toolchain (it
stops at 100 errors after 2:05, peak RSS 11.07 GB). A true clean build of this
port succeeds in 4:41 at peak RSS 4.54 GB (3,221 jobs). The final dependency
extractor runs in 39.9s at peak RSS 5.52 GB.
Verification
lake build LeanPool.GapCVPlake exe runLinterwith all 69 GapCVP modules enumerated explicitlylake exe lint-stylewith all 69 GapCVP modules enumerated explicitlylake exe mk_all --checkLeanPool.leancollision compile#print axiomsfor all four endpoints: onlypropext,Classical.choice,and
Quot.sound