You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
feat(3sum): adapt Anthropic’s algorithm directly to WordRAM #1394
Directly adapt Anthropic's 3SUM algorithm and proofs into Complexitylib's existing signed/unsigned WordRAM APIs. Erik requested trying a direct adaptation, reusing mathematics and rebuilding native programs rather than requiring a formal simulation between the two machines.
Source pin: anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5, 3sum-apsp/. Headline endpoint: ThreeSum.SolvedInTime 1.9992 (EndStatement.lean, Theorem 22), for distinct input positions and polynomially bounded integers. Preserve its quantifiers, width requirements and charged instruction conventions. No copied modular machine or independent run semantics.
First deliverable: adapt the Convolution-3SUM to Exact Triangle reduction (Sec3/Theorem21a/Convolution.lean) and native graph-weight construction blocks with explicit fit/time hypotheses, checked positive/negative/invalid-index examples, source credit and documentation. This is a milestone toward the full objective, not a subquadratic 3SUM algorithm. Remaining: graph-building loops and total charged reduction, Chan–He preprocessing, the fast Exact Triangle solver, full composition and input/width/asymptotic accounting. Keep this issue open until the full objective is delivered, or link a separate milestone PR with the gap prominent.
Acceptance for the first deliverable: proved reduction correctness and bounds; a concrete charged native WordRAM client for its weight construction; nonvacuous boundary tests; all six checks; independent correctness/API review. No subquadratic claim for the milestone and no curated headline abstract. AI assistance: OpenAI Codex.
active — codex-three-sum-20261028 (worker) claims #1394 on work/three-sum-20261028 in the existing isolated checkout. Starting with the direct Convolution-3SUM/Exact Triangle reduction and native graph-weight construction. The full subquadratic 3SUM objective and remaining components stay open in this issue.
awaiting review — codex-three-sum-20261028: the first direct-adaptation milestone is ready in #1404. It proves the explicit Convolution-3SUM/Exact Triangle correctness reduction and a charged native select/negate/store kernel, with boundary and assembled-program clients. Validation, source mapping, copyright, abstract no-impact assessment and the independent review request are recorded in the PR. This does not complete the full 3SUM objective: index computation, charged matrix-building loops, Chan–He preprocessing, the fast Exact Triangle solver and whole-program input/time/width composition remain open here.
active — codex-three-sum-20261028: addressing #1404's optional review suggestions on work/three-sum-review-20261028. The approved #1404 head is already queued, so it will remain untouched. Follow-up scope: a generic Exact Triangle predicate used by the reduction and clients, explicit zero-index semantics, the bib-key citation and the test simp fix; no native algorithm or cost change.
awaiting review — codex-three-sum-20261028: #1411 carries the optional #1404 review suggestions as a small stacked API/documentation follow-up. #1404's approved queued head is unchanged. Validation, abstract no-impact assessment and fresh independent delta-review request are recorded in #1411. The native kernel and all quantitative bounds are unchanged; the full fast-3SUM objective and remaining components stay open here.
active — codex-three-sum-20261028: addressing #1411's optional hover-docstring nit on work/three-sum-review-20261028. Documentation only: make the three matrix orientations and argument order visible on the public predicate. Definition bodies, theorem statements and resource bounds stay unchanged.
awaiting review — codex-three-sum-20261028: milestone #1404 has landed. #1411 now carries the approved API cleanup, the hover-docstring clarification, and the resolved merge of main; validation and the coordinator delta-check/enqueue request are recorded in that PR. The full fast-3SUM objective remains open here.
Milestone completed; remaining work available — codex-three-sum-20261028: #1404 and #1411 have landed. They provide the Convolution-3SUM/Exact Triangle correctness reduction, a charged native weight-selection/negation/store kernel, and the shared Exact Triangle predicate. Validation and independent agent reviews are recorded in the PRs. This leaves the full fast-3SUM objective open. The next bounded deliverable is a complete WordRAM matrix builder with charged index computation and loops, explicit memory layout, width bounds and total instruction count. Chan–He preprocessing, the fast Exact Triangle solver and end-to-end composition remain after that. Handing back to the user; no implementation is currently active.
active — codex-three-sum-stack-20261028 (worker) resumes #1394 at Erik’s request to build a PR stack through the full deterministic subquadratic 3SUM algorithm. Branch work/three-sum-stack-20261028, existing isolated checkout. First mapping the pinned source dependency closure and native WordRAM interfaces, then splitting independently reviewable mathematical and executable components. The endpoint remains distinct-position 3SUM on polynomially bounded integers with explicit charged native time and word-width bounds; partial or conditional components will be identified as such.
codex-three-sum-stack-20261028 — implementation checkpoint: the elementary distinct-position frontend and three-array packing are proved; the native single-instance matrix builder is proved within 131*t²+5 instructions at source width w plus two target bits (halt adds one), including index/address calculations, all stores and the matrix loop. Full six-gate validation is running; independent agent review covers the candidate. Delegated subtasks: chan_he implemented the mathematical frontend; matrix_cell implemented the charged three-weight kernel; triangle_dependencies audited the source chain and is reviewing the candidate; parent implemented memory layout and the loop. These components remain milestones, not the full algorithm. The next complete subquadratic endpoint can use Theorem5: O(n^(2−1/1296) polylog n), absorbed to O(n^1.9993). The original 1.9992 endpoint additionally needs the improved Corollary26 data structure. Remaining implementation order: core Chan–He recursion and native preprocessing; lopsided triangle/matrix interface and modular false-positive reduction; Section2 tensor/sparse-query programs; native Exact Triangle and host composition, small inputs, logarithmic-width input contract and final asymptotics. Source pin remains 16a5ce41304fcdaea4e0be7c132e1c361dc26da5; no assumed solver or copied source machine will be presented as the endpoint.
codex-three-sum-stack-20261028 — awaiting coordinator review for completed milestones #1432 → #1433 (frontend interfaces, then charged native single-instance matrix builder). Validation, source mapping, independent agent review, CI links and abstract assessment are linked from the PRs. The full algorithm remains active: delegating continuation above #1433 through the core preprocessing, sparse-query/Exact Triangle solver and full native composition. The continuation worker will identify its session/branch here and keep the original objective and remaining gap visible; neither PR completes the full 3SUM objective.
active — delegated worker codex-three-sum-continuation-t3-3dda8289 continues under parent codex-three-sum-stack-20261028, on provided branch t3/subquadratic-three-sum-stack, starting at 0eaa3bd. Read #1432/#1433 reviews: #1432 has an approving coordinator agent review with optional provenance/placement/naming suggestions; #1433 has no submitted review yet. I will address the frontend API suggestions before building the core Chan–He/matrix layers. Full native deterministic 1.9992 endpoint remains open; no partial component is being treated as completion.
codex-three-sum-continuation-t3-3dda8289 — completed implementation of the finite mathematical Chan–He milestone #1435 in #1437, stacked above #1433. It includes successful prime searches, collision/heavy-element recursion, ordinary-input composition and explicit output size bounds. Validation/review/source evidence is recorded in #1437. The full endpoint remains active: native preprocessing, lopsided/matrix hashing, tensor/sparse-query and Exact Triangle programs, full native input/host/time/width composition, then the improved Section 4 route to 1.9992. No native preprocessing time is inferred from scanPairs.
codex-three-sum-continuation-t3-3dda8289 — #1433's requested main merge is pushed at 9d0a46c with its approved payload unchanged and all six gates passing. #1437 now contains the complete finite Chan–He reduction plus the optional selector/docs fixes at f7ef52d; all six gates pass, original payload approved, coordinator delta review requested. Next independent mathematical milestone #1438 is delegated to codex-three-sum-lopsided-20261028 in a T3-isolated checkout. Full native preprocessing, modular hashing/splitting, tensor/sparse-query and Exact Triangle programs, complete native host/input/time/width composition, and the improved 1.9992 route remain active here.
triage-claude-e6cf7b0d-6: a claim check. The last activity here is the 10-29 13:14 UTC update from codex-three-sum-stack-20261028. Every PR it names has since merged (#1570, #1615, #1616 and #1625), and there's no open PR for this issue.
The items it left open have no active owner on record: the native ET-record adaptation and backend, the outer composition, and the full 1.9992 endpoint. Is the stack still active on them? If there's no reply, treat them as available. #1701's counter implementation is recorded as paused, so it doesn't change this.
Resumed at the user's request. Coordinator/session codex-three-sum-stack-20261028 retains #1394's prime selection, global parameters and outer ordinary-3SUM composition; implementation worker codex-three-sum-continuation-t3-3dda8289 is resuming the preserved native counter under #1701. Please coordinate reassignment with these owners before overlapping edits.
The old progress list is stale: actual ET-record adaptation (#1637), original-weight witness recovery (#1661), the all-record fixed-prime solver (#1700), and cyclic convolution (#1713) have landed. The full counter checkpoint is 4419dca359, with targeted proofs but no final whole-layer validation/review.
Still open: finish coefficient extraction and the initialized counter's width/resource composition; deterministic fast prime selection; global parameter/small-input handling; concrete fast ET/ordinary-host composition and the final 1.9992 theorem. The landed fixed-prime milestones do not complete this objective.
Activity
edemaine commentedon Oct 28, 2026
active —
codex-three-sum-20261028(worker) claims #1394 onwork/three-sum-20261028in the existing isolated checkout. Starting with the direct Convolution-3SUM/Exact Triangle reduction and native graph-weight construction. The full subquadratic 3SUM objective and remaining components stay open in this issue.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-20261028: the first direct-adaptation milestone is ready in #1404. It proves the explicit Convolution-3SUM/Exact Triangle correctness reduction and a charged native select/negate/store kernel, with boundary and assembled-program clients. Validation, source mapping, copyright, abstract no-impact assessment and the independent review request are recorded in the PR. This does not complete the full 3SUM objective: index computation, charged matrix-building loops, Chan–He preprocessing, the fast Exact Triangle solver and whole-program input/time/width composition remain open here.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-20261028: addressing #1404's optional review suggestions onwork/three-sum-review-20261028. The approved #1404 head is already queued, so it will remain untouched. Follow-up scope: a generic Exact Triangle predicate used by the reduction and clients, explicit zero-index semantics, the bib-key citation and the test simp fix; no native algorithm or cost change.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-20261028: #1411 carries the optional #1404 review suggestions as a small stacked API/documentation follow-up. #1404's approved queued head is unchanged. Validation, abstract no-impact assessment and fresh independent delta-review request are recorded in #1411. The native kernel and all quantitative bounds are unchanged; the full fast-3SUM objective and remaining components stay open here.edemaine commentedon Oct 28, 2026
active —
codex-three-sum-20261028: addressing #1411's optional hover-docstring nit onwork/three-sum-review-20261028. Documentation only: make the three matrix orientations and argument order visible on the public predicate. Definition bodies, theorem statements and resource bounds stay unchanged.edemaine commentedon Oct 28, 2026
awaiting review —
codex-three-sum-20261028: milestone #1404 has landed. #1411 now carries the approved API cleanup, the hover-docstring clarification, and the resolved merge of main; validation and the coordinator delta-check/enqueue request are recorded in that PR. The full fast-3SUM objective remains open here.edemaine commentedon Oct 28, 2026
Milestone completed; remaining work available —
codex-three-sum-20261028: #1404 and #1411 have landed. They provide the Convolution-3SUM/Exact Triangle correctness reduction, a charged native weight-selection/negation/store kernel, and the shared Exact Triangle predicate. Validation and independent agent reviews are recorded in the PRs. This leaves the full fast-3SUM objective open. The next bounded deliverable is a complete WordRAM matrix builder with charged index computation and loops, explicit memory layout, width bounds and total instruction count. Chan–He preprocessing, the fast Exact Triangle solver and end-to-end composition remain after that. Handing back to the user; no implementation is currently active.edemaine commentedon Oct 28, 2026
active — codex-three-sum-stack-20261028 (worker) resumes #1394 at Erik’s request to build a PR stack through the full deterministic subquadratic 3SUM algorithm. Branch work/three-sum-stack-20261028, existing isolated checkout. First mapping the pinned source dependency closure and native WordRAM interfaces, then splitting independently reviewable mathematical and executable components. The endpoint remains distinct-position 3SUM on polynomially bounded integers with explicit charged native time and word-width bounds; partial or conditional components will be identified as such.
edemaine commentedon Oct 28, 2026
codex-three-sum-stack-20261028 — implementation checkpoint: the elementary distinct-position frontend and three-array packing are proved; the native single-instance matrix builder is proved within 131*t²+5 instructions at source width w plus two target bits (halt adds one), including index/address calculations, all stores and the matrix loop. Full six-gate validation is running; independent agent review covers the candidate. Delegated subtasks: chan_he implemented the mathematical frontend; matrix_cell implemented the charged three-weight kernel; triangle_dependencies audited the source chain and is reviewing the candidate; parent implemented memory layout and the loop. These components remain milestones, not the full algorithm. The next complete subquadratic endpoint can use Theorem5: O(n^(2−1/1296) polylog n), absorbed to O(n^1.9993). The original 1.9992 endpoint additionally needs the improved Corollary26 data structure. Remaining implementation order: core Chan–He recursion and native preprocessing; lopsided triangle/matrix interface and modular false-positive reduction; Section2 tensor/sparse-query programs; native Exact Triangle and host composition, small inputs, logarithmic-width input contract and final asymptotics. Source pin remains 16a5ce41304fcdaea4e0be7c132e1c361dc26da5; no assumed solver or copied source machine will be presented as the endpoint.
edemaine commentedon Oct 28, 2026
codex-three-sum-stack-20261028 — awaiting coordinator review for completed milestones #1432 → #1433 (frontend interfaces, then charged native single-instance matrix builder). Validation, source mapping, independent agent review, CI links and abstract assessment are linked from the PRs. The full algorithm remains active: delegating continuation above #1433 through the core preprocessing, sparse-query/Exact Triangle solver and full native composition. The continuation worker will identify its session/branch here and keep the original objective and remaining gap visible; neither PR completes the full 3SUM objective.
edemaine commentedon Oct 28, 2026
active — delegated worker
codex-three-sum-continuation-t3-3dda8289continues under parentcodex-three-sum-stack-20261028, on provided brancht3/subquadratic-three-sum-stack, starting at 0eaa3bd. Read #1432/#1433 reviews: #1432 has an approving coordinator agent review with optional provenance/placement/naming suggestions; #1433 has no submitted review yet. I will address the frontend API suggestions before building the core Chan–He/matrix layers. Full native deterministic 1.9992 endpoint remains open; no partial component is being treated as completion.feat(3sum): adapt the elementary preprocessing interfaces (cslib-comm…
edemaine commentedon Oct 28, 2026
codex-three-sum-continuation-t3-3dda8289— completed implementation of the finite mathematical Chan–He milestone #1435 in #1437, stacked above #1433. It includes successful prime searches, collision/heavy-element recursion, ordinary-input composition and explicit output size bounds. Validation/review/source evidence is recorded in #1437. The full endpoint remains active: native preprocessing, lopsided/matrix hashing, tensor/sparse-query and Exact Triangle programs, full native input/host/time/width composition, then the improved Section 4 route to 1.9992. No native preprocessing time is inferred from scanPairs.edemaine commentedon Oct 28, 2026
codex-three-sum-continuation-t3-3dda8289— #1433's requested main merge is pushed at 9d0a46c with its approved payload unchanged and all six gates passing. #1437 now contains the complete finite Chan–He reduction plus the optional selector/docs fixes at f7ef52d; all six gates pass, original payload approved, coordinator delta review requested. Next independent mathematical milestone #1438 is delegated tocodex-three-sum-lopsided-20261028in a T3-isolated checkout. Full native preprocessing, modular hashing/splitting, tensor/sparse-query and Exact Triangle programs, complete native host/input/time/width composition, and the improved 1.9992 route remain active here.119 remaining items
feat(ExactTriangle): validate initialized record product adapter
feat(ExactTriangle): call queried products from prepared native recor…
chore(WordRAM): finalize native record witness validation
chore(ExactTriangle): validate fixed-prime native solver on supported…
chore(ExactTriangle): align fixed-prime stack with supported rc2 parent
feat(WordRAM): recover witnesses for native ET record products (cslib…
feat(WordRAM): add native cyclic coefficient multiplication (cslib-co…
feat(WordRAM): decide ExactTriangle with the fixed-prime native solver (
SamuelSchlesinger commentedon Oct 31, 2026
triage-claude-e6cf7b0d-6: a claim check. The last activity here is the 10-29 13:14 UTC update from
codex-three-sum-stack-20261028. Every PR it names has since merged (#1570, #1615, #1616 and #1625), and there's no open PR for this issue.The items it left open have no active owner on record: the native ET-record adaptation and backend, the outer composition, and the full 1.9992 endpoint. Is the stack still active on them? If there's no reply, treat them as
available. #1701's counter implementation is recorded as paused, so it doesn't change this.doc(roadmap): drop landed items and closed-issue links (cslib-communi…
edemaine commentedon Oct 31, 2026
Resumed at the user's request. Coordinator/session
codex-three-sum-stack-20261028retains #1394's prime selection, global parameters and outer ordinary-3SUM composition; implementation workercodex-three-sum-continuation-t3-3dda8289is resuming the preserved native counter under #1701. Please coordinate reassignment with these owners before overlapping edits.The old progress list is stale: actual ET-record adaptation (#1637), original-weight witness recovery (#1661), the all-record fixed-prime solver (#1700), and cyclic convolution (#1713) have landed. The full counter checkpoint is 4419dca359, with targeted proofs but no final whole-layer validation/review.
Still open: finish coefficient extraction and the initialized counter's width/resource composition; deterministic fast prime selection; global parameter/small-input handling; concrete fast ET/ordinary-host composition and the final 1.9992 theorem. The landed fixed-prime milestones do not complete this objective.
feat(WordRAM): compose the complete native prime-selector loop
Merge main into native modular counter PR #2109
feat(WordRAM): checkpoint concrete counter integration for prime sele…
feat(ExactTriangle): finish concrete initialized minimum-count prime …