SIDE QUEST 08 / MATHEMATICS / AGENTIC RESEARCH

Agentic Maths

Can coding agents make useful progress on neglected open mathematics when every claim must survive deterministic verification?

An experiment in research design: choose computationally searchable, falsifiable problems; split the attack across exact solvers, search programs and proof attempts; then make verification—not model confidence—the gatekeeper.

STATUSPROTOTYPE · RESEARCH
RUNSBROWSER · VERIFIED COMPUTATION
INTERACTIVE BELOW ↓
INTERACTIVE P05 CONSTRUCTIONPROOF DRAFT · VERIFIED BASES
INTERACTIVE PROTOTYPEVISUAL: PROOF ARCHITECTURE

This explains the constructive induction recorded in the repository. It does not independently execute or certify the full proof in your browser.

P05 / LANE-LIFTING CONSTRUCTION

Turn one interval into three non-colliding modulus families.

The final construction recursively splits [1,n] into residue lanes modulo 3. One lane is a single mod-3 class, one receives a ×3 lift of an N3 cover, and one receives a ×3 lift of a smaller M3 cover.

LANE 1M3(334)×3 recursive M3v₃(modulus) ≥ 2
LANE 2N3(333)×3 N3 coverv₃(modulus) = 1
LANE 3one classx ≡ 3 (mod 3)modulus = 3
n = 1,000→3 residue lanes→distinct by 3-adic valuation→2 recursive M3 levels before base range
P BASE17–108direct finite bridge
N3 BASE41–81no modulus divisible by 3
M3 BASE109–326all moduli divisible by 3
INTERACTIVE RESEARCH PORTFOLIOP05 CANDIDATE · P02 + P06 ACTIVE
INTERACTIVE PROTOTYPERESEARCH: VERIFY-FIRST / MIXED MATURITY

This is a public research dashboard, not an autonomous proof oracle. A computation is labeled only for the finite region actually checked; mathematical claims require an independent verifier or complete proof.

AGENTIC MATHS / RESEARCH PORTFOLIO

Give agents problems that can prove themselves wrong.

The experiment is methodological: select neglected open problems with finite attack surfaces, let coding agents pursue genuinely different methods, and require machine-checkable evidence before a result is allowed to survive.

CONJECTURE→SEARCH→VERIFY→CRITIC
P05 / CANDIDATE THEOREM

Minimum-modulus covers

For every n ≥ 17, can an IRDCS be constructed with minimum modulus at least 3?

Candidate all-n construction complete for this phase. The proof draft uses lane lifting and 3-adic separation, 351 verified finite bases, four checker paths in clean-room reproduction, mass verification, and a primary-source prior-art audit. No human expert review yet; no public SOLVED claim.
PROOF DRAFTLane lifting + N3/M3 induction gives a constructive cover for every n ≥ 17, conditional only on finitely checked base certificates.FINITE BASEThe proof uses 351 explicit certificates: P 17–108, N3 41–81, and M3 109–326.CROSS-CHECKED622 stored base certificates were rechecked; constructed covers passed for every n=17…100,000, plus n up to 10⁸ in selected large tests.CLEAN ROOMAn independent implementation rebuilt the construction from the proof text and verified every n=17…20,000 plus large samples.NOVELTY GATEPrimary-source audit through 2026-09-25 found no prior statement of the main all-n theorem. Current label: apparently novel pending expert review; publication status remains not ready for a public solved claim.
THE RULE

Negative search results mean only “no example in the explicitly searched finite region.” A claimed discovery must carry a machine-checkable certificate or rigorous proof, an independent verifier, and a fresh prior-art check.

P05 / CANDIDATE THEOREM

A finite search became an all-n construction.

P05 asks whether every length n ≥ 17 admits an incongruent restricted disjoint covering system whose minimum modulus is at least 3. The current proof draft answers yes by combining finite verified bases with recursively closed N3 and M3 families. The construction separates lifted modulus families by 3-adic valuation. The main theorem is labeled apparently novel pending expert review—not solved or published.

P05 / VERIFICATION

The finite burden is explicit and reproducible.

The proof depends on 351 base certificates: P for 17–108, N3 for 41–81, and M3 for 109–326. Clean-room regeneration and multiple checkers accepted the required bases; generated covers were swept through n=100,000 and spot-checked to 10⁸. A primary-source audit through September 25 found no earlier statement of the main all-n theorem, while correctly identifying partial prior art for the stronger all-moduli-divisible-by-3 family.

P02 / ACTIVE SEARCH

Broad mining gave way to structure.

P02 asks for a rational Diophantine septuple. Phase 1 built independent exact verifiers and certified extension machinery. Phase 2 accumulated 2,224 verified sextuples from 6,672 certified mining units without producing a new almost-septuple or septuple candidate, so broad mining was stopped. The active route now targets elliptic-curve hub compatibility and parametric families instead of spending compute on a low-yield search.

P04 / OPEN FRONTIER

The negative frontier moved, but the problem remains open.

P04 asks for an exact congruence cover in which every class hits at least three times. Two independent code bases find no example for n ≤ 108; published prior work already covered n ≤ 105, making 106–108 the new cross-checked finite extension. Structural proof drafts show increasingly strong constraints, including a computer-assisted result forcing some modulus ≤ n/6. None of this proves global nonexistence.

P06 / ACTIVE FOUNDATION

The next discovery target is a bijection, not a brute-force witness.

P06 targets an explicit uniform bijection between Gog and Magog trapezoids. A current prior-art audit confirms the general problem remains open and found no known k=3 bijection; k=1 and k=2 are the solved baselines. The research program starts by reproducing known maps and exact counts, then compares statistics and searches for low-description-length invertible rules that generalize beyond the training sizes.

FIELD NOTE / METHOD

Verification—not model confidence—is the gatekeeper.

The project deliberately favors problems with falsifiable finite attack surfaces. Exact solvers, independent verifiers, mutation tests, proof critics and fresh literature checks are used to separate an interesting computational signal from a publishable mathematical claim.

RESEARCH DISCIPLINE

What counts as progress

  1. Formalize first.

    Turn an informal open question into an executable definition before optimizing anything.

  2. Cross-check methods.

    Where practical, make structurally different solvers agree—rather than trusting one clever implementation.

  3. Attack the verifier.

    Mutation tests, planted controls and independent critics are part of the research system because a fast wrong UNSAT is worse than no result.

  4. Keep claims narrow.

    A finite search is evidence about that finite region. A theorem needs a proof. A potentially novel result needs a fresh literature and attribution check.

CURRENT FRONTIER

Four problems, four different research modes.

P05 is in candidate-theorem review; P02 is an active Diophantine structure search; P04 is an open problem with a strengthened finite nonexistence frontier and structural constraints; P06 has entered foundation work for bijection synthesis. The point is not to make every branch look solved—it is to make the evidence level legible.

$ agentic-maths --statusP05 ............. candidate theorembases ........... 351 verifiedprior art ....... no main-theorem match foundexpert review ... pending---P02 ............. active / no septuplecorpus .......... 2,224 sextuplesP04 ............. open / no H=3 through 108P06 ............. active foundation / k=3 targetrule ............ claim only what evidence supports
← All side quests
← Bedtime Story EngineAll Side QuestsKryptos K4 →