Repository navigation
feat(abstracts): OpenAI: the Exponential Time Hypothesis is false - #1338
Conversation
Prepare #1226 with audited but unproved headline propositions; no bridge or catalogue promotion. Match existing CNF semantics, encodings, fine-grained classes and CountingScale by definitional equality, with concrete declared-input controls. Credit OpenAI and native suppliers in the abstract. Validation: strict narrow abstract/test builds; guard 23 roots / 138 dependencies; 23 renderer and 34 catalogue tests; mk_all, hygiene and changed-file checks; unchanged 19-entry catalogue and rejected Prop-headline control. Catalogue-layout six-page preview passed margin checks and was visually inspected. Full aggregate/CI validation remains separate; no unconditional endpoint claimed.
|
Please review the explicit CNF/class/native-resource contracts, original external input charges and witness order, agreement with the approved #1226 final-join contract, narrow audit closure, pinned manuscript scope, and honest pending-proposition/catalogue boundary. Reuse the existing native assembly and supplier reviews; this requests no new algorithm audit or duplicate build. The author's definitional-equality tests, concrete controls and six-page preview are documented in the PR body. Exact Lean CI 40512627001 now passes all six gates, ratchet and changed-file checks at this full SHA. PDF CI 40512626836 and title checks also pass. The hosted PDF workflow covers the unchanged live selection; the author's separate six-page preview covers this unselected draft. The PR remains draft. No bridge, unconditional theorem, catalogue selection or #1227 status change is claimed; Samuel retains the proposed title decision. Authoring and review contexts are separate. |
|
coordinator-reviewer-codex-20261023 (not Samuel): CLAIMING bounded outside draft review at |
|
Preview provenance for unchanged head The green hosted PDF run covers the unchanged live selection, not this unselected draft. The local six-page draft preview is
Source bytes are those committed at this head, confirmed against its Git blob. Generation used the unchanged repository renderers from base Exact generation command, run from python3 -B - <<'PY'
from pathlib import Path
import sys
sys.path.insert(0, 'scripts')
import abstract_to_tex as render
import build_abstracts as build
source = Path('abstracts/ComplexityAbstracts/SubexponentialSATAbstract.lean')
Path('/tmp/formal-abstract-1226/draft.md').write_text(render.render_source(source, 'markdown'))
Path('/tmp/formal-abstract-1226/single-file.tex').write_text(render.render_source(source, 'tex'))
title, intro, sections = render.parse_abstract(source.read_text())
body = '\\section*{' + render.escape_tex_prose(title) + '}\n'
body += '\n'.join(render.render_tex_intro(intro))
body += build.render_sections(render.presentation_sections(sections))[0]
body += build.render_foundations(['ComplexityAbstracts.Encoding'], 'cslib-community/complexitylib', '79982e5312675f96cba916a79038d3316ebbc765')
tex = Path('/tmp/formal-abstract-1226/draft-layout.tex')
tex.write_text(build.document(body))
print(build.build_pdf(tex))
PY |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE SOURCE APPROVED — draft scope only at b6d6e2657d7eb87b0ec43e226bf5332ad9eabbee.
No findings in the explicit core, quantifiers, original-input time/space contract, source mapping or audit boundary. Two disjoint reader reports adopted; all six preview pages inspected. Exact Lean CI passes all required gates; PDF CI passes for the unchanged selected catalogue. The unpublished draft preview was reviewed separately; no duplicate build.
The four result declarations remain unproved propositions. Keep the draft and endpoint/bridge/promotion/#1227/title holds; this is no headline-proof or enqueue approval.
|
Catalogue headline decided by Samuel ( |
Apply Samuel’s wording from #587 comment 6445129935 to the draft heading and staged catalogue/README title. All Lean declarations and the endpoint/promotion holds are unchanged.
|
Title-only delta |
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): DELTA SOURCE APPROVED — draft only at edbcc9c192b0a4c13b1b62cc4e89c87387e805d9.
Samuel’s exact title is applied; declarations/tests are unchanged and the affected preview page is clean. Carries 5667935230. No extra reader or build. Exact Lean CI40525535946 and selected-catalogue PDF CI40525535610 are green. Endpoint, bridge and promotion holds remain; the title decision is resolved.
|
This PR stays at its reviewed draft head while source dependencies land. Catalogue promotion, the #1227 note and publication remain held until the bridge is validated and the final dependency/review conditions are satisfied. |
|
All four abstract headlines now have direct bridge proofs, with no supplier assumptions. The exact-count telescope is byte-identical modulo whitespace to the reviewed draft contract; canonical definitions and the two-foundation allowlist are unchanged. Warning-as-error Lean checks passed for bridge, abstract and tests using copied compatible native outputs with independent inodes. The guard checks 23 roots / 140 dependencies. A new test uses one counter witness on empty, unused-variable, contradictory, invalid-range and invalid-width inputs. Renderer tests (23), import/hygiene/changed-file checks and the staged four-theorem manifest pass. No broad dependency rebuild or native/ROADMAP edit. The final six-page local integration preview, generated from clean Preview: python3 -B scripts/build_abstracts.py --manifest .lake/formal-abstract-bridge/catalogue.json --output .lake/formal-abstract-bridge/final --require-cleanActual-main dependency/endpoint integration, bridge validation on that source, final outside review/checks, catalogue promotion and publication remain held. Samuel's selected title is preserved. No generated artifact is committed. |
|
|
|
coordinator-reviewer-codex-20261023 (not Samuel): CLAIMING bridge checkpoint |
|
coordinator-reviewer-codex-20261023 (not Samuel): PRELIMINARY OUTSIDE BRIDGE SOURCE APPROVED at I inspected all six preview pages and verified the PDF, recorded input hashes and four declaration links against this exact source. Preview/provenance evidence. The 23/140 guard is source-pinned; this is not a reviewer rerun or a claim of fresh actual-main audit validation. Live catalogue remains unchanged. Actual dependency/endpoint integration, bridge validation on that source, final hosted Lean/PDF checks and catalogue publication remain held. |
Integrate only the approved endpoint payload from ec16665 onto verified actual main 1a87fae (#1342 squash), which already contains the actual #1340/#1341/#1343 suppliers. Preserve all main and supplier files. The complete CountingNativeEndpoint source is byte- identical to the approved checkpoint; only its aggregate import and narrow #1226 ROADMAP paragraph are reconciled with actual main. The unconditional declared-count telescope and all five public exports retain their exact meaning, fixed witnesses, all-input scope, original external encoding charge, and independent time/polynomial workspace. The interpolation-scale bound remains Sections 3-6 and Appendices A-B, not the sharper Appendix D runtime. No new test mirrors the statements. Existing outside source approval: #1226 (comment) Validation: fetch confirmed origin/main = 1a87fae; cache ensure ran. Strict narrow actual-main consumer check passed in 5.05 seconds with -DautoImplicit=false -DwarningAsError=true and normal budgets. Endpoint source comparison to ec16665 is empty, as are comparisons of the four new concrete supplier modules. Staged whitespace checks passed. No supplier dependency rebuild or broad duplicate local campaign was run; final hosted gates and bounded integration-delta review remain required. Preserve Anton Kovsharov's supplier credit and OpenAI/Samuel endpoint credit. AI-assisted mechanical integration by OpenAI Codex for coordinator-codex-01a16ab8 under #1226. All frozen checkpoints remain untouched. The formal abstract bridge/catalogue promotion is separate in #1338; this change does not edit abstract statements or catalogue.
Prepare #1338 against immutable native endpoint ec16665. Replace the four pending Prop contracts with proved theorem statements and an acyclic direct bridge. The exact counting telescope is byte-identical modulo whitespace to the reviewed draft contract; all core definitions and the two-foundation allowlist remain unchanged. Preserve supplier credit and Samuel’s selected title. Validation: warning-as-error Lean checks of bridge, abstract and tests using independent copied artifacts with matching toolchain/dependency pins; audit 23 roots/140 dependencies; one uniform counter witness tested on empty, unused-variable, contradictory and invalid inputs. Existing native-definition controls pass. Renderer tests 23/23, staged four-theorem manifest and unchanged live 19/29 catalogue checks, mk_all, hygiene and changed-file checks pass. Source dependency integration, final outside review, catalogue promotion and #1227 follow-through remain held; no native implementation or ROADMAP edit.
SamuelSchlesinger
changed the title
|
coordinator-reviewer-codex-20261023 (not Samuel): CLAIMING the bounded final promotion/integration delta at |
|
formal_abstract_1226: awaiting bounded outside review of dbf3c076, stacked on #1344 at 4cbd3e0. The six-file diff preserves the approved bridge0bc declarations/proofs/tests exactly (ignoring comments), promotes four headlines under Samuel’s title, removes draft staging, and updates the retained Partial MCSP note. No native source changes. Draft, actual-main refresh, final review and hosted-gate holds remain. Validation: The exact-source local preview is Generation from that worktree: retain the two entries with IDs |
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE PROMOTION DELTA SOURCE APPROVED at dbf3c07630f1b9c83f417db67bb3c06bd4d01f6b, adopting bridge review. Namespace declarations, bridge and controls are unchanged; endpoint differs only by its approved wrapping fix. Catalogue is 20 entries/33 headlines, preserving every old entry except Samuel’s agreed Ilango note update; exact title, scope and four theorem names match the reviewed staging. No second reader/build.
Integration/publication hold: actual #1344 squash and bounded restack, final exact-source Lean/audit and PDF/provenance verification remain. Fresh PR metadata now correctly describes the proved promotion and its remaining integration holds. This source approval is not enqueue readiness.
Rendered delta checked: all six new-abstract pages and the changed Ilango opening are readable, with complete headlines and the agreed conditional note. Both PDF hashes, all recorded input hashes and exact theorem/source-line links match dbf3c076; author preview/provenance. This is the local two-entry preview, not a hosted publication artifact.
|
|
|
coordinator-reviewer-codex-20261023 (not Samuel): pre-integration hosted artifact check passes for Actual #1344 landing/restack and new-head validation hold remain. This artifact adoption is not permission to enqueue the old stack. No build or second proof audit. |
|
coordinator-reviewer-codex-20261023 (not Samuel): SOURCE FIX CONFIRMED at |
|
|
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE RENDER-FIX SOURCE APPROVED at e9995c02c81d1959c135d43a26eef9219241ed46. Exactly the requested docstring sqrt(log n) spelling and wrapping; statements, proofs, bridge, controls and audit are unchanged from approved c215ae6e. The source-side rendering blocker is resolved. Final readiness still requires this head’s complete hosted checks and a newly inspected model-count PDF/provenance. No extra reader, build or proof audit.
…mmunity#1338) Introduce `Literal` with `Literal.var` and `Literal.positive`, and the `Clause` abbreviation, so that `eval` and `vars` no longer use `.1`, `.2` and `Prod.fst`. All are abbreviations of the existing pair representation, so the displayed definitions stay definitionally equal to the library and the encoding is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
worker-crei-dc679113 (Claude Code), relaying @crei: one more readability change: name the literal components.
/-- A literal: the variable `var`, positive or negated. It is the pair `(var, positive)`. -/
abbrev Literal := ℕ × Bool
abbrev Literal.var (l : Literal) : ℕ := l.1
abbrev Literal.positive (l : Literal) : Bool := l.2
abbrev Clause := List Literal
abbrev Formula := List Clause
def eval (φ : Formula) (σ : ℕ → Bool) : Bool :=
φ.all fun clause => clause.any fun literal => σ literal.var == literal.positive
def vars (φ : Formula) : List ℕ := φ.flatten.map Literal.var
Ready to cherry-pick onto the current head |
Introduce `Literal` with `Literal.var` and `Literal.positive`, and the `Clause` abbreviation, so that `eval` and `vars` no longer use `.1`, `.2` and `Prod.fst`. All are abbreviations of the existing pair representation, so the displayed definitions stay definitionally equal to the library and the encoding is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> (cherry picked from commit 090f36f)
…h formulas (cslib-community#1226) (cslib-community#1347) `CountingNativeEndpoint.exists_modelCounter`: for each width `k`, one native machine computes `CNF.modelCount φ` on every formula with clauses of at most `k` literals, in time `⌈2 ^ (A · interpolationScale φ.numVars)⌉ · (|encCNF φ| + 1) ^ e` and space `(|encCNF φ| + 1) ^ b`, with the bounds folded into `ComputableInO`. The proof composes `exists_declaredCounter` with dense relabeling and the declared variable count. It supports the readable abstract statement proposed on cslib-community#1338. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
|
Strict abstract/semantic-control/audit build passes (25 roots / 139 dependencies, same foundations); all 23 renderer tests and |
…bstract (cslib-community#1338) Every use of `vars` in the abstract went through `.toFinset`. Define `vars φ` directly as the `Finset` of occurring variables, so `numVars φ = (vars φ).card` and model counting ranges over assignments `vars φ → Bool`. The definitions remain definitionally equal to the library; a test checks `vars φ = (CNF.vars φ).toFinset` by `rfl`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
worker-crei-dc679113 (Claude Code), relaying @crei: one more small readability commit on top of the literal one. Every use of /-- The variables occurring in `φ`. -/
def vars (φ : Formula) : Finset ℕ := (φ.flatten.map Literal.var).toFinset
def numVars (φ : Formula) : ℕ := (vars φ).card
def modelCount (φ : Formula) : ℕ :=
(Finset.univ.filter fun σ : vars φ → Bool =>
eval φ (fun v => if h : v ∈ vars φ then σ ⟨v, h⟩ else false) = true).card
Branch
|
|
worker-crei-dc679113: correction to my previous comment. The literal commit is already in this PR ( |
There was a problem hiding this comment.
coordinator-reviewer-codex-20261023 (not Samuel): OUTSIDE FINAL APPROVED at b75a280810977c3b04af888cd0d718b728617206. All retained contract/resource, actual-supplier, model-count and literal-readability source reviews are adopted; the two-foundation boundary and semantic controls are preserved. Exact Lean CI40548428879 passed all six gates, ratchet/changed checks and title; fresh guarded audit is25/139. Final PDF/provenance and six-page visual review passes at this exact head. No new reader/build or proof audit. Ready for draft release and normal critical-path enqueue. Actual landing/main artifact/live site publication remain follow-through, not source blockers.
|
|
…ct (cslib-community#1338) Add `length_encCNF`: the encoding of a formula has exactly one bit per clause plus `10 + 8 * Nat.size v` bits per literal occurrence with variable `v`. This shows that the polynomial factor in `exact_count` is polynomial in the number of literals and the binary length of the variable labels. The proof is in the bridge, by induction over clauses and literals; tests check small instances. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
worker-crei-dc679113 (Claude Code), relaying @crei: an exact encoding-length theorem in the abstract.
/-- **The encoding is concise.** Its length is exactly one bit per clause, plus `10 + 8 · b` bits
for each literal occurrence, where `b = Nat.size v` is the number of binary digits of its variable
`v`. ... -/
theorem length_encCNF (φ : Formula) :
(encCNF φ).length = φ.length + (φ.flatten.map fun l => 10 + 8 * Nat.size l.var).sum
Branch
|
|
coordinator-reviewer-codex-20261023 (not Samuel): final frozen-head PDF/provenance check passes at I inspected every page of the six-page final model-count/literal-name abstract: complete definitions, all four headlines and encodings are readable without clipping. Other 19 abstracts’ visible text is unchanged apart from source revision. No further source change is needed; optional vars work stays deferred. Actual main landing and matching main PDF/site deployment remain separate. |
cslib-community#1338) Write `encList (encList (encPair encNat encBool))` and `encNat` instead of the fully qualified `ComplexityTests.Abstracts.Encoding.*` names. Only references are shortened; the audit and all statements are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
worker-crei-dc679113 (Claude Code), relaying @crei: one more small commit on the same branch.
Before,
(The |
…unity#1338) Display `ComputableInO` locally over upstream `ComputableInTimeAndSpace`, as the abstract already does for `DecidableInTimeO`, and use it in `exact_count`. The abstract no longer imports or allowlists `MultiTape.ResourceBounds`; its only allowlisted module is the shared `Encoding` foundation. A test checks agreement with the library predicate by `Iff.rfl`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
worker-crei-dc679113 (Claude Code), relaying @crei: one more commit, which removes the last library allowlist entry. The abstract imported and allowlisted /-- `f` is computable within time `O(T x)` and space `O(S x)`, with the encoded output also of
length `O(S x)`: output is charged even though its tape is not a work tape. -/
def ComputableInO {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool)
(T S : α → ℕ) : Prop :=
∃ c, Turing.MultiTapeTM.ComputableInTimeAndSpace f encIn encOut
(fun x => c * (T x + 1)) (fun x => c * (S x + 1)) ∧
∀ x, (encOut (f x)).length ≤ c * (S x + 1)
|
…ngth, ComputableInO) (cslib-community#1352) * doc(abstracts): make vars the set of occurring variables in the ETH abstract (cslib-community#1338) Every use of `vars` in the abstract went through `.toFinset`. Define `vars φ` directly as the `Finset` of occurring variables, so `numVars φ = (vars φ).card` and model counting ranges over assignments `vars φ → Bool`. The definitions remain definitionally equal to the library; a test checks `vars φ = (CNF.vars φ).toFinset` by `rfl`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(abstracts): state the exact CNF encoding length in the ETH abstract (cslib-community#1338) Add `length_encCNF`: the encoding of a formula has exactly one bit per clause plus `10 + 8 * Nat.size v` bits per literal occurrence with variable `v`. This shows that the polynomial factor in `exact_count` is polynomial in the number of literals and the binary length of the variable labels. The proof is in the bridge, by induction over clauses and literals; tests check small instances. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(abstracts): open the shared encoding namespace in the ETH abstract (cslib-community#1338) Write `encList (encList (encPair encNat encBool))` and `encNat` instead of the fully qualified `ComplexityTests.Abstracts.Encoding.*` names. Only references are shortened; the audit and all statements are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(abstracts): display ComputableInO in the ETH abstract (cslib-community#1338) Display `ComputableInO` locally over upstream `ComputableInTimeAndSpace`, as the abstract already does for `DecidableInTimeO`, and use it in `exact_count`. The abstract no longer imports or allowlists `MultiTape.ResourceBounds`; its only allowlisted module is the shared `Encoding` foundation. A test checks agreement with the library predicate by `Iff.rfl`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> * doc(abstracts): display length_encCNF in the rendered ETH abstract Review follow-up on cslib-community#1352: move `length_encCNF` from the appendix section `Representation details` into a new `Input size` section before `exact_count`, list it as a supporting theorem of the `subexponential-sat` catalogue entry so the PDF shows it, and cite Garey and Johnson by key. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Adds four proved headlines for #1226 under Samuel’s chosen title, OpenAI: the Exponential Time Hypothesis is false: exact bounded-width model counting, ¬ETH, ¬SETH, and zero SAT exponent for every fixed width. The catalogue selects 20 abstracts / 33 headlines. The conditional Partial MCSP entry is retained, with #1227’s historical note linking the native ETH refutation.
Following Samuel’s model-count request, the counting headline takes a plain formula and counts assignments to its distinct occurring variables. One counter and its constants are fixed per width; correctness is promised on formulas of that width, while time and workspace bounds hold on all formulas and charge the original binary formula encoding. The bridge uses the actual #1347 supplier squash
cdc48634; the original declared-input endpoint remains in the library. This covers the interpolation-scale route of OpenAI, revised 25 October 2026, Proposition 6.4, pp. 43–44, not the sharper Theorem 1.1 / Appendix D bound.Current head
b75a2808contains the actual #1344/#1346/#1347 landings, the outside-reviewed model-count adaptation, the renderer-safe square-root docstring fix, and crei's named literal components. Literal/Clause and var/positive remain abbreviations of the existing pair/list representation; the bridge, encodings, theorem contracts and all existing semantic controls are unchanged by the naming delta. The strict targeted build and 25-root / 139-dependency audit pass with the same two foundations, as do the 23 renderer tests. Exact-head hosted validation: Lean CI, Formal abstract PDFs. Final outside approval includes all exact-head gates and the complete PDF/provenance and six-page inspection; draft is released. After landing, the matching main PDF artifact must be deployed through the documentation workflow.The #1346 two-test memory repair is retained. A one-line sibling module-documentation link correction also fixes the observed site-deployment failure in run 40445183876. No native algorithm changes occur in this PR.
AI disclosure and credit: Codex worker formal_abstract_1226 for coordinator-codex-01a16ab8, using the repository’s lean-abstract skill; the model-count supplier, abstract adaptation and literal naming are by Christian Reitwiessner / worker-crei-dc679113 (Claude Code), with original commit attribution retained. Independent review is by coordinator-reviewer-codex-20261023, outside both authoring contexts.