Mathmaxxing

Reproducible research infrastructure for AI-assisted work on open mathematical problems. (All rights reserved. Ask for permission before using this project.)

The active portfolio has ten level-2 bounded research tracks: a 237-point cap in F_3^7, S(6) >= 537, an ideal Prouhet--Tarry--Escott size-11 target, S(3,6,46), perfect-cuboid fibers, Hadamard order 668, R(5,5), constant-weight codes, certified odd-perfect-number branches, and covering arrays and related design records. A candidate is only data until independent exact verifiers accept it, and it is not a novelty claim until the current literature has been checked.

The Schur track tests whether [1,537] admits a six-coloring with no monochromatic solution of x + y = z. The schur/ package reconstructs the published coloring of [1,536], verifies it two ways, and emits a transparent 537-instance CNF. A SAT witness would improve the lower bound; an UNSAT solver return is not accepted without an independently checked proof log.

As of 2026-07-25, the supported public affine bound is 236 <= a(7) <= 288; the 288 upper bound is from a preprint, while the peer-reviewed upper bound is 292. This repository reproduces and independently verifies the known 236-point construction. It has not found 237.

Repository map

• AGENTS.md — durable research and verification rules.
• LUNA_HELPERS.md — reusable Codex/Luna thread registry.
• DECISIONS.md — architectural and mathematical decisions.
• RUNBOOK.md — experiment lifecycle and recovery procedure.
• automation/ — persistent review-thread config and durable review prompt.
• experiments/ — run conventions; bulk generated runs remain ignored.
• schemas/ — machine-readable experiment contracts.
• scripts/ — deterministic local evidence and receipt tools.
• gpu/ — the batched conflict-relaxed CUDA method and run instructions.
• capset/ — exact certificate parsing, two verifiers, the published 236-point construction, bounded search baselines, and exact shell exclusions around that construction.
• schur/ — the published S(6) >= 536 coloring, strict certificates, two independent verifiers, and a direct SAT encoding for the 537 pilot.
• status/checkpoints/ — curated, evidence-backed milestones.
• status/reviews/ — cost-gated progress reviews.
• systemd/ — five-minute user-timer units for the cheap conditional gate.

The source-backed status, record-changing math-agent evidence audit, and publication path are in bibliography/.

Exact local commands

Verify a certificate with the independent pair or triple algorithm:

python3 -m capset CERTIFICATE.json --method pair
python3 -m capset CERTIFICATE.json --method triple

Run a bounded CPU search:

python3 -m capset.search_cli \
  --seed 0 --iterations 100 --destroy-count 96 --strategy shuffled \
  --certificate-out /tmp/cap-best.json \
  --summary-out /tmp/cap-summary.json

Recompute the exact neighborhood exclusion:

python3 -m capset.shell_cli \
  --output /tmp/shell-exclusion-f3-7-v8.json

Benchmark the next unresolved shell with an atomic per-prefix checkpoint:

run_id="$(date -u +%Y%m%dT%H%M%SZ)-shell27-prefix-benchmark"
python3 -m capset.shell_shard_cli \
  --checkpoint artifacts/shell27-prefixes.json \
  --manifest "experiments/runs/$run_id/manifest.json" \
  --removals 27 --start 0 --max-prefixes 10 \
  --memo-entries 100000

Repeat with a fresh manifest path. The checkpoint resumes at next_prefix; its .prev sibling retains the preceding generation. A completed invocation verifies only the prefixes it advanced, and a shell is excluded only after adjacent checkpoint ranges cover every prefix without a candidate. The memo-entry limit bounds memory while retaining cached vertex-cover answers across atomic prefixes in one invocation. Cache resets change reuse only, not branching or feasibility.

An optional direct SAT formulation provides a structurally different exact cross-check:

uv pip install --python .venv/bin/python -r requirements-sat.txt
run_id="$(date -u +%Y%m%dT%H%M%SZ)-shell24-direct-sat"
.venv/bin/python -m capset.shell_sat_cli \
  --output "experiments/runs/$run_id/result.json" \
  --manifest "experiments/runs/$run_id/manifest.json" \
  --checkpoint "artifacts/shell24-direct-sat.json" \
  --removals 24 --solver cadical195 --symmetry-prefixes

The SAT model directly chooses exactly 24 removed base points and 25 outside points, then encodes every base–base–outside, base–outside–outside, and outside-only progression. It does not use the common-cover recursion. The optional prefix mode reuses only the verified two-point symmetry partition, then decides every prefix with the independent SAT clauses and retains learned clauses across assumptions. It also adds implied binary clauses for outside-point pairs whose matching union needs more than 24 base removals; these strengthen propagation without changing the solution set. CaDiCaL runs in repeated conflict-budget chunks so signals return to Python and finalize the run manifest without discarding learned clauses.

The exhaustive matching, maximum-clique, and shared-cover calculation proves that no 237-point cap can differ from the published 236-cap by 26 or fewer removed base points. The completed shell-24 through shell-26 checkpoints are curated in experiments/shell24-prefix-exclusion-v1.json through experiments/shell26-prefix-exclusion-v1.json. This is a local Hamming-neighborhood result, not an upper bound on all caps in F_3^7.

The terminating, timeout-bounded worker and Fly command templates are documented in fly/README.md. The current implementation is CPU-only; an RTX 3080 does not accelerate it.

The separate conflict-relaxed CUDA method and RTX 3080/Modal commands are in gpu/README.md. It keeps fixed-size 237-point candidates with temporary conflicts and uses batched group convolution to score all point swaps.

Reproduce and verify the published Schur coloring, then emit the direct six-color CNF for [1,537]:

python3 -m schur reproduce-536 --output /tmp/s6-536.json
python3 -m schur verify /tmp/s6-536.json --method both
python3 -m schur cnf --maximum 537 --colors 6 \
  --output /tmp/s6-537.cnf

The deterministic CNF has 3,222 variables and 441,145 clauses with the safe color-permutation break color(1) = 0. Its clauses encode exactly one color per integer and forbid every monochromatic Schur triple, including x = y.

modal_cpu_benchmark.py is the one-container harness used for the matched Modal/Fly efficiency test. That test authorized production Modal CPU only while a reservation remains entirely in the first $10 monthly usage tier.

Local checks

python3 -m unittest discover -s tests -v
python3 scripts/progress_snapshot.py --hours 2
git diff --check

The review gate depends on pinned local ccusage 20.0.18. It reads local Codex session logs and calculates model-specific API-equivalent cost offline; it does not upload session contents. The five-minute check itself makes no model call; only a passing $25 gate resumes the persistent Luna xhigh review thread.

Paid external compute is independently capped for each problem track at 1% of that level-2 task's and its level-3 descendants' cumulative registered ccusage. Inspect a track's lifetime allowance with:

python3 scripts/external_compute_budget.py --track capset-237 status
python3 scripts/external_compute_budget.py --track schur-s6 status
python3 scripts/external_compute_budget.py --track pte-ideal-11 status

Fly, rented GPU, or other paid jobs must reserve their conservative maximum before launch and settle actual provider cost afterward. A successful budget reservation is necessary but does not replace any required launch approval.

Modal GPU work and justified CPU work use the same workspace-wide pre-credit usage calculation. The matched 5,706,679-step CPU benchmark measured 296,804 steps/s on Modal, 248,310 on Fly shared, and 274,065 on Fly performance. At the first-tier 1/8 weight, Modal cost about $0.000035 effective versus $0.000062 and $0.000335 for Fly. Production Modal CPU is therefore allowed only while its entire reservation stays in the first $10 tier; the 1/4 tier already makes Fly shared slightly cheaper for this workload. GPU reservations remain allowed in later tiers. The weighted effective cost—not undiscounted provider list cost—consumes the 1% allowance.

Backup

The working tree is included as mathmaxxing in Projectmaxxing's existing encrypted Restic backup set. That user timer snapshots about every 15 minutes to the established offsite SFTP repository and applies the existing daily, weekly, and monthly retention policy. Git object stores remain excluded, so the public Forgejo remote and Restic source backup are complementary.