ACTIVE-CLAIMS: live coordination between concurrent sessions
Read this before launching an agent, a prover submission, or a build in hunts/frontier_math/. HANDOFF.md is the serial channel (session to session, across time).
Every document this laboratory publishes, not only the parts
that worked. 915 documents, 220,517 lines, listed straight off
git ls-files. The tree's housekeeping is not here: the
instructions its workers read, the between-session handoffs, the harness's
notes on its own trials. Those stay in the repository, which is public, and
anyone cloning it to send a change reads them there.
| 915 | documents |
| 220,517 | lines |
| 5 | shelves |
Most of this is working record rather than finished writing: routes opened and abandoned, tables sized wrong and resized, corrections to our own corrections. It is here because a laboratory that publishes only its results has published the smallest and least checkable part of what it did. Titles and descriptions are the files' own first heading and opening paragraph, so this index cannot describe a document as something other than what it says it is.
The transplant into the source paper's chain: the working paper, the obligation ledger, every route opened and every one closed. The largest single body of working record in the tree, and the least finished.
Read this before launching an agent, a prover submission, or a build in hunts/frontier_math/. HANDOFF.md is the serial channel (session to session, across time).
What modification of the world would preserve the appearance of this result while making its interpretation false?
2026-08-13/14. Measurements only. Nothing here is kernel-checked, nothing here is evidence about RH, and nothing here closes blocker 2.
Status: WITHDRAWN / FALSIFIED UNDER CURRENT FORMULATION Date withdrawn: 2026-08-15
Sprint 1 draft, 2026-08-12. Lane 1 step 2 of PIPELINE.md. This is the specification a later session turns into an Aristotle submission for Zeta23Ext/Bridge.lean.
The 0.672529 candidate is withdrawn. Its first required algebraic lemma is false. The failure occurs before taper, truncation, census, bootstrap, or LP questions can affect the result.
Verdict: the discrepancy resolves, your measurements reproduce exactly, and the transfer does not survive, for a reason that is not in your data, because it is outside your scan window.
An audit run from a fresh clone by a session that did not build any of the instruments below, against the source paper's own text.
Record of a measurement-and-proof exchange with the theorem-proving service during submission 9 , 2026-08-13.
No positive portion of the ordered-gap floor follows from the paper's existing unconditional zero-side inputs. The obstruction is quantitative, not merely a missing sign argument.
Date: 2026-08-13. Reads: gram_form.py (the three-term form), kpair_identity.py (the identity and the joint search), PROOF-LEDGER.md defect #20.
2026-08-15. Reads: K2-ROUTE.md (the state it supersedes in part), RETENTION-PROBLEM.md (the k=1 proof whose machinery this transplants), gram_form.py / kpair_identity.py (the identity…
A route to proving lattice extremality, worked out far enough to say exactly what is proved, under which hypotheses, and what is missing.
Level 2 of the hierarchy in INTERACTION-CONTROL-REPORT.md asks for state retaining one off-line pair marked against two consecutive on-line gaps, an exact object giving projective…
No, and for a sharper reason than incompatible offsets: the level-1 envelope is not attained in even one cell.
Theta is positive at the single-pair reduction, by a wide measured margin (the scan stays safe through theta = 0.9), and the mechanism is exact.
Level 3 left two named gaps in promotion order: a bound on the adversary's value valid over all configurations (its worst case was measured over two families), and the multi-pair slack…
The directive set two promotion gates: rigorous enclosure of the level-4 cells, and closure of the general multi-pair interaction.
Level 5 ended with the combined per-pair budget overdrawing by 0.151–0.387 of slack at every depth and two named reversing estimates. Both landed:
Level 6a's theta_full = 0.02 carried the label "at unit pair density". This level asks what happens when the density is the adversary's to choose, and the answer has a structure worth…
1. The joint cap exists and closes the entire swept density axis. The named theorem object of level 6b, an on-line-configuration-free upper bound on the joint profit against a pair cluster…
The operator's instruction: go find previously unknown mathematics adjacent to the 10 August 2026 paper (More than two thirds of the zeros of the Riemann zeta function lie on the critical…
Date: 2026-08-13. Purpose: price the asset before anything is built on it publicly. Companion to NOVELTY-CHECK.md, which killed a different claim from this hunt on 2026-08-12.
Date: 2026-08-12. Purpose: avoid a false novelty claim.
O9Check.lean had never been elaborated (§5 explains why: nothing imports it, and it was additionally missing the import of its own damageIv).
Status: ready to build. Scoping is done (O9-SCOPING.md, o9_scoping.py, 17 pins in test_o9_scoping.py). Nothing below is research; every number it needs already exists.
2026-08-13. Follows O9-2D-STATUS.md §0, which recorded that decide +kernel refuted the generated O9 table on 7 of 9 chunks.
2026-08-13. Found by trying to perform the final assembly and failing. Nothing here is kernel-checked, nothing here is evidence about RH.
Date: 2026-08-13. Code: o9_scoping.py, test_o9_scoping.py (17 pins). Reads: RETENTION-PROBLEM.md §4 (the obligations) and §7 (the arithmetic).
Written 2026-08-12. The plan for finishing the Lean arm of the transplant chain (and the one adjacent higher_xi batch), arranged as four independent lanes plus a standing collection loop.
Zeta Lab, August 2026. Working paper: candidate result, external review invited.
Audited local state: add40513fb1919ea4d00f87bdb61b5b433f7801d.
Evidence for the meta/ arm, written from the job history rather than from impressions. This hunt ran nine submissions to Harmonic's Aristotle service on 2026-08-12/13 (a tenth is still…
Status: CLEAN KILL. The unconditional candidates 0.6725124, 0.672529, and 0.6725318 are withdrawn.
Target: remove the hypothesis hsep from Retention.retention_separated_of_le and the hypothesis n ≤ 3 from Retention.retention_le_three, in the package hunts/frontier_math/zeta23ext…
State as of 2026-08-13. The single-pair (k = 1) retention inequality is closed at hardened grade with no separation hypothesis (ledger, four instruments plus a coordinator reproduction).
INTERACTION-CONTROL-REPORT.md closed with: "No decimal search should run before level 1 below has an unconditional zeta constraint that excludes the obstruction family." This report…
Clone: git clone --depth 1 https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean.git →…
Written 2026-08-13 as a handoff, because the working record grew to 29 markdown files and 8131 lines and buried the one thing that matters. Read this file.
Scope: fit against the four open items, the bandlimited nonnegative-kernel inequality over exponential sums, uniform in configuration; the finite→infinite-lattice bridge and the…
The candidate reading's most dangerous unproven step, "the transplant lemma" connecting theta_full (proved at the hunt's window) to the Cheer-Goldston floor (computed with the…
A Lean 4 package depending on the source paper's formalization (anthropics/zeta-23-lean, pinned by commit; toolchain and Mathlib pin inherited from it) into which the frontier_math formal…
Exploratory studies, explicitly not results. A hunt records a claim before any control has been run against it, which is why each one carries a mission stating what it may touch.
Adopted on probation, 2026-08-11 (ROADMAP.md, "The outside memos, triaged", adopted build 3). A HuntSpec is a fenced block inside a hunt's MISSION.md that states, in a form a validator can…
A hunt is an exploratory study: a scoped directory where an agent or a person pursues one specific idea, with the understanding that most such ideas fail.
Successor to Hunt #72 (hunts/r_662b12, run 31e8a4f2), whose reported +25pp robustness signal was withdrawn by independent audit (in-sample rule on the 28 labels, scrambled-text control…
Frozen 2026-08-22, before any predictor is fitted against the robustness labels. The descriptive curation finding is not a fitted predictor and does not depend on this document; this…
AIMO Interpretability Challenge at NeurIPS 2026 (Codabench competition 16180), technical report. Every number below is reproducible from the organizers' public datasets by…
Status: report-ready (reframed 2026-08-22); Main-track entry is a legal model-identity prior; Small-track entry is the always-non-robust constant; leaderboard learned-method arm stays…
Formal-native research probe, run 2026-08-23. One obligation, not a formalization of a paper. The success criterion set for it was did formal feedback change the mathematical understanding…
Ainta's seven-point simple-zero bound (paper/riemann.tex at ainta/zeta-simple-zeros commit 040c5e899e658aed7b56a2a87f501798fe10761d, cited A with line numbers), stated and proved in Lean on…
Every figure is labelled VERIFIED (read off a file or a build), MEASURED (computed this session), INFERRED, or NOT MEASURED.
Two outside groups are hill-climbing the same finite certificate for the proportion of simple zeros on the critical line: Ainta (ainta/zeta-simple-zeros, a GPT-5.6 Sol research draft with…
Gohms's run is the published verifier with two constants changed. Nothing else in it is new, and the issue says so.
Environment for every run below: macOS (Darwin 25.5.0, Apple Silicon), Python 3.14.7, python-flint 0.9.0, ainta/zeta-simple-zeros at commit 040c5e899e658aed7b56a2a87f501798fe10761d…
Every figure is labelled VERIFIED (read off a file or a build this session), MEASURED (computed this session), INFERRED, or NOT MEASURED.
Written 2026-08-23. Companion to this hunt's MISSION.md, which reproduces the finite certificates and which was still uncommitted in a sibling worktree when this landed, so this file may…
Agent: bridge/S8 (branch bridge/S8, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/S9 (branch bridge/S9, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/finite (branch bridge/finite, from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/pinching (branch bridge/pinching, forked from bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
Agent: bridge/skeleton (branch bridge/skeleton). Cap: 3 submissions. Used: 0 of 3.
AMTOPA/zeta-exact-pressure holds the leading public claim for the proportion of simple zeros, 0.6734164909714992949..., first in the fifteen-claim ranking this laboratory's own field audit…
Target pinned at AMTOPA/zeta-exact-pressure, commit 7253fdcab9366af45b8c8caf44e408c0af44a1a7, 2026-08-13 17:26:37 +0800.
Every run of this hunt, including the ones that produced nothing and the one that had to be killed.
Scope: hunts/arch_cover/ only. Nothing outside this directory is modified. Status: exploratory. Nothing here is a result about the Riemann Hypothesis.
Nothing here is a result about the Riemann Hypothesis. This is a measurement of how the three pieces of the Weil functional balance, on two families of test functions, with enclosures where…
Hunt #136, lane "assembly", 2026-10-21. Status: lane output, revised after verifier round 1, unreviewed by any person.
Hunt #136, lane eulerstep, 2026-10-21. Revised twice the same day after two rounds of an adversarial verifier: the first listed seven issues, all minor; the second listed one major issue…
Hunt #136, followups lane. Nothing here is a result of this laboratory: it is a map of other people's claims, none of them refereed.
Hunt #136, Lean lane, 2026-10-21. Status: done for this wave. This page is written by the only agent in the hunt's first workflow that runs lake or lean. The lane ran in two sessions.
Numbering note, 2026-10-30. In this hunt's files "#134" names seven_eighths_pin/, the 13/15 ceiling hunt, which was opened as #134 and is case-logged as hunt #139.
Hunt #136, lane probe, 2026-10-21, revised after two verifier passes the same day. Status: pricing, not proving; unreviewed by any person.
Hunt #136, lane rowcounts, 2026-10-21, repaired after an independent verifier's review (section 10). A lane report inside an open hunt; no person has reviewed it.
Created 2026-10-26, when the lane was resumed in place by the owner's decision of that day. The first wave kept no RUNS.md.
Hunt #136, lane b78-amplification, 2026-10-21. Lane output, unreviewed by any person. Nothing here is a result until the case log in hunts/README.md says how the hunt ended.
Hunt #136, lane b78-amplification, 2026-10-21. Lane output, unreviewed by any person. Nothing here is a result until the case log in hunts/README.md says how the hunt ended.
Hunt #136 , referee lane b78-referee, wave 1, 2026-10-21; repaired the same day after an adversarial review (section 7).
Third application of the lab's procedure for a published computer-assisted bound (after the two seven-point simple-zero certificates of Hunt #79): reproduce the bound from its own verifier…
Archive bloch-computations-1.0.0.zip (Zenodo 10.5281/zenodo.21975862), sha256 bdaa1ff3…408e7 verified, all 28 entries of CHECKSUMS.sha256 verified.
Environment for the local runs: macOS (Darwin 25.5.0, Apple Silicon), CPython 3.12.12 in a fresh venv from the archive's requirements.txt (python-flint 0.9.0, numpy 2.5.1, scipy 1.18.0), on…
Target: the standard Riemann Hypothesis, every zero of zeta in 0 < Re < 1 has Re = 1/2. Proof and disproof are equally acceptable.
RH remains unresolved. This is an ordinary derivation, exact rational controls, a bounded numerical experiment, and eight finite matrix signs checked with Arb enclosures.
Research disposition: unresolved. No resolution of RH, no novelty assertion, and no outside mathematical review. The proof text is an ordinary derivation with named classical dependencies.
Is there any mathematically nontrivial correspondence between the twelve chromatic pitch classes and the colour wheel, beyond the fact that both can be drawn on a circle?
This laboratory publishes its working record, corrections included. That is a policy, and a policy is a claim about behaviour. Nobody had measured the behaviour.
2026-09-10. Grade: measured, and one headline is withdrawn by its own control. This is not mathematics and nothing in it bears on RH .
id: claim_halflife-2026-09-09-corpus hunt: claim_halflife started: 2026-09-09T23:20-05:00 finished: 2026-09-09T23:40-05:00 ran: - git rev-parse --is-shallow-repository - git fetch…
One fixed positive Fourier density gives two real multisets with identical power traces at every order and different numbers of simple points.
This note derives a finite-dimensional extension of the counting mechanism in Proposition 2.1 of Youness Lamzouri, A new proof that more than 2/3 of the zeros of the Riemann zeta function…
Started 2026-09-05 under the operator's instruction to pursue substantive mathematical research with the available provers and compute resources.
This note gives a finite counting improvement whose denominator uses a narrow fourth moment. Its first Montgomery-Taylor profiles do not produce a positive numerator.
The repeated-index corrections below are exact. Applying separate bounds to their terms can lose information, and power traces alone do not determine every corrected cycle statistic.
This is a finite statement about a conjugation-invariant multiset. It gives no new asymptotic bound for zeros of zeta. The arithmetic cost is stated below.
Finite counting improvements are proved here. Their application to a stronger zeta-zero proportion remains open.
The hunt produced finite counting inequalities and an exact counting distinction invisible to the complete spectrum. It does not improve the laboratory's asymptotic zeta-zero proportion.
Base commit: 6139de6173ea7e538db6097170a1ccfe93f311cb. The dates below record the research day, not reconstructed wall-clock times.
There is one even, nonnegative, compactly supported probability density whose Fourier kernel gives two full-rank, four-point Gram matrices with identical spectra and different distinct…
Under the finite signed-vector hypotheses of FINITE-THEOREM.md, matched second and third moment limits alone cannot improve the second-moment counting proportion.
Chain lane of hunt #147, written 2026-10-21 and repaired the same day after an adversarial review.
Opened 2026-10-21. Hunt #147. Route 5 of the campaign the owner directed on 2026-10-21. The task that opened this hunt proposed #140; the campaign orchestrator assigned #147 because #138 to…
Chain lane of hunt #147, 2026-10-21, repaired the same day after an adversarial review. Reading only; every citation Q:ID is re-read from its hashed source by test_chain.py (see CHAIN.md…
Status: closed at landing, 2026-10-31. No claim promoted, no bound on Lambda stated, nothing here bears on RH .
Each lane appends its own entries; neither edits the other's. Timings are wall clock on the shared swarm box (32 vCPU), single process, under whatever load the other workflows were putting…
Status (2026-10-26, later the same day): built and preregistered. The literature record is DH_LITERATURE.md, the gate code is dh_gate.py with test_dh_gate.py, and the preregistration is…
Written and committed 2026-10-26, before the gate was run. The commit that adds this file precedes every gate run.
Written and committed 2026-10-31, at landing, before any stage-2 box was decided. Stage 1 (DH_GATE_PREREG.md, commit 2ba8cbba3) is not changed by this file: its six boxes, its parameters…
Searched 2026-10-26, before any DH correction term was written (DH.md, step 3). The question: is there a published Riemann-Siegel-type or other effective approximation, with explicit error…
Status: built and checked against two independent routes to H_t, at small x and (Milestone 1b) at large x where the correction term is tested sharply; the printed Table 1 row 2 bound is…
Scope: hunts/decay_law/. Nothing outside this directory is modified, apart from the case-log entry this hunt owes in hunts/README.md. Status: exploratory.
Nothing here is a result about the Riemann Hypothesis. This is a measurement of one ratio, on two compact families, on one window. Grade: measured.
id: decay_law-2026-10-30 hunt: decay_law started: 2026-10-30T21:03:00Z finished: 2026-10-30T21:05:34Z ran: - python hunts/decay_law/decay.py outcome: the kill fired on the margin and on the…
Status, 2026-09-14: closed at measured grade.
Grade: measured throughout. Nothing here is a theorem, and nothing bears on RH .
Estimate written before launch: the probe reads one existing JSON artifact and evaluates a finite cosine-hyperbolic sum on a grid of a few hundred depths, so seconds on a laptop, no…
Base commit: 85efdcb2b4f8255caed8dbac0961c28361abd413. Status: bounded construction, not an established heat-flow comparison.
Status: candidate ordinary argument with enclosure-carrying numerical steps. Independent Muse and Gemini reviews found no analytic or implementation defect in the complete packet.
Base 85efdcb2b4f8255caed8dbac0961c28361abd413 has successful GitHub Actions tests run 34913353458 and full run 35095988548, read through gh in this session.
Base: origin/main at ef4e056 , worktree branch hunt/forage-2026-10-08. Status: exploratory probe; nothing here is a result .
Status: exploratory probe, complete. Nothing here is a result . Narrow frame s = 1/2 + iz throughout; the parent hunt's wide-frame values are the narrow ones times four.
All runs on 2026-10-08 in the hunt/forage-2026-10-08 worktree, Python 3.13 from the repository's .venv (python-flint 0.9.0, rigor.BACKEND = python-flint), one core, no CI, no Lean build.
Every claim this run touched, whether the run generated it or the repository already carried it. A claim with no disposition is an unfinished claim, not a true one.
The point of a graveyard is that a laboratory which remembers why ideas failed becomes harder to fool.
The metric the operator named is legitimate research output per unit of scarce human judgment. That needs a denominator, and the denominator is only useful if it is not gamed.
Agent persona: the Directorate (an internal organization with deliberately conflicting roles, not one agent) Scope: hunts/director_run/ for artifacts; docs/25-the-director-run.md for the…
Written before the first result came back, so the allocation can be scored against what actually happened. Amendments are appended with a timestamp, never edited in place.
Exploratory. Nothing here is a result (see hunts/README.md).
A bounded measurement run. One quantity, two precisions.
zeta/epstein.py caps working precision in one place inside the rival interface it hands the battery: epstein_interface"count_zeros_box" passes dps=min(d, 20) both to count_zeros_box and to…
Opened 2026-08-14. A bounded measurement, not a claim about zeta and not a result. Nothing here has been through a control.
A bounded measurement run, opened 2026-08-14 by the operator. One number, at two precisions, plus the sweep needed to read those two numbers against a scale.
A bounded measurement run. One quantity, two precisions.
Status: probe, complete. At 0.8 + 85.7i the capped precision does not return a worse answer, it returns no answer: 3.1e-33 where the converged value is 1.6e-58, a factor of 1.9e25 and not…
Opened 2026-08-13. Nothing in this directory is a result.
Nothing in this directory is a result. hunts/README.md classifies the area: a hunt is exploratory, and this one was opened to state a single mechanism for the Riemann Hypothesis and then…
Nothing here is a result about the Riemann Hypothesis. This is the report of one attack on one mechanism, and the mechanism did not survive it. No progress on RH was made.
id: epp_herglotz-2026-08-19-run1 hunt: epp_herglotz started: 2026-08-19T00:00Z finished: 2026-08-19T00:00Z ran: - .venv/bin/python hunts/epp_herglotz/probe.py outcome: the mechanism stated…
An adversarial audit by a separate agent with no part in producing the result. Seventeen attacks. Eleven landed.
Two hunts in this tree have already met this. hunts/gate5_p6_c/probe.py derives the mechanism in a comment and writes the constant down:
2026-09-10. Grade: measured, against an oracle the routine shares no code with. Nothing here bears on RH : it is a measurement of an implementation.
id: epstein_height-2026-09-09-surface hunt: epstein_height started: 2026-09-09T23:47-05:00 finished: 2026-09-10T00:20-05:00 ran: - .venv/bin/python hunts/epstein_height/probe.py --heights…
An adversarial audit run by a separate agent with no part in producing the result, given the write-up and the repository and told to break the claim rather than review it.
Issue #93 records a measured observation and one open question. The observation: a nonzero log-derivative coefficient at a composite is a failure of multiplicativity read off the zeros, and…
This hunt may not write zeta/, tests/ or docs/. What follows is the change it would make if it could, stated precisely enough to be argued with.
2026-09-10. Grade: measured. The load-bearing quantity is a, an exact integer count of representations of 1, and everything else here is downstream of it.
id: euler_defect_axis-2026-09-09-entitlement hunt: euler_defect_axis started: 2026-09-09T23:00-05:00 finished: 2026-09-10T00:10-05:00 ran: - .venv/bin/python…
docs/15-the-f1-discovery-engine.md writes up seven exploratory prototypes (ontology/01_f1_geometry.py … 07_the_imposter_gauntlet.py) and closes with a Reality Check that dials the rhetoric…
Exploratory. Nothing in hunts/ is a result or evidence . What follows is measured, at the sizes stated, with the instruments in this directory.
id: f1_engine_controls-2026-08-21-open hunt: f1_engine_controls started: 2026-08-21T03:20Z finished: 2026-08-21T15:50Z ran: - .venv/bin/python hunts/f1_engine_controls/ln2_law.py --max-n…
run_experiment.py sweeps a one-parameter family F_kappa, kappa from 0 to 1, and records a factorization_defect together with a max_position_residue.
Agent Persona: The Hunter Your Scope: hunts/factorization_vs_position/
This file has been through an independent adversarial audit and did not come out unchanged. A different model (OpenAI Codex, gpt-5.6-sol), working in an isolated directory outside this…
The n-point pressure certificate family gives, for each n, the bound
lim{n -> infinity} Phi_n = H = 0.6725007036794116 DERIVED, exact sup_n Phi_n <= 0.675142509660254 AUDIT, VERIFIED here configuration ceiling 0.6818286874638 deficit at the family's best >=…
id: family_wall-2026-08-23-analytic-limit hunt: family_wall started: 2026-08-23T15:40-05:00 finished: 2026-08-23T19:10-05:00 ran: - .venv/bin/python hunts/family_wall/verify_chain.py…
You are auditing a mathematical claim that the person who wrote this believes is TRUE and wants you to attack. Your job is refutation, not confirmation.
The isolated repository's history, oldest first:
The supporting argument is false as written. Steps 2 and 3 both omit necessary conditions. Step 2 reverses direction when its numerator is negative.
Each decimal below is interpreted exactly as printed. The corresponding directed interval evaluations are in intervals-requested.json.
Hunt #148, steps 2 and 4. Status: the F_7T transplant of the base probe is built; its original, Poisson and Euler representations agree exactly at every checked degree triple, up to total…
Opened 2026-10-21. Hunt #148. A lane of the campaign the owner directed on 2026-10-21 (route 6 of its second wave: a second probe in F_qT).
Status: closed 2026-10-26. Disposition: candidate refuted at the stated parameters (the biquadratic probe over F_13T has no scalar local identity); the transfer of that verdict to S4 over Q…
Hunt #148, step 5. Status: exact algebra and ball-enclosed zeros at the stated parameters; files produced on branch hunt/ff-probe, not landed.
All runs are single-process Python on the swarm box (32 vCPU, 115 GiB, shared), started at nice 10, with the 1-minute load average between 56 and 100 during the session (other workflows'…
Hunt #148, step 3. Verdict: no. In F_13T the coefficients of the biquadratic (n = 4) theta function at squarefree indices are computable, and they do not vanish identically beyond small…
Hunt #148, step 1. Status: the cited formulas are pinned by brute force at q = 7, n = 3, degree at most 3, with the corrections listed below; files produced on branch hunt/ff-probe, not…
Hunt #148. Status: the cross-check run of 2026-10-26 (15 items) reproduced every exact number it recomputes; no row disagrees with the primary run (section 2 lists the rows that record…
Occasioned by discovering, on 2026-08-24, a wave of public repositories created 2026-08-11 and 2026-08-12, a week before this laboratory's own seven- and eight-point work, carrying…
This laboratory's number is not the leading one, and never was. Our best figure, 0.6730529829896288 (eight-point, bridge proved in Lean), is tenth of fifteen public claims for this…
One night, one host (one laptop, no cloud, no Lean build). Every external repository was read or replayed read-only; nothing was posted, opened, commented, forked or starred anywhere.
Agent Persona: The Hunter (unsupervised-fun edition, second outing) Scope: hunts/flow_repair/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md.
Run of 2026-08-07, probe.py, raw numbers in results.json. Probe language throughout: measured, observed.
The original stages ran on the authoring host on 2026-08-07; their wall-clock times are the seconds fields of results.json.
This directory preserves the arithmetic and terminal verification status of the 2026-09-05 experiment.
Lab module/toolchain port and exported-proof comparison verified. The stronger proof and its interface build on Lean 4.35.
Current status : the Lean kernel build of the c = 2330/10^6 candidate has been run and passed, locally by this laboratory, on Modal.
Recorded 2026-09-28. This is the laboratory's kernel build of the generated FourPointCand package at the pinned toolchain. It is not external review and it is not a Palomar registration.
- Verdict: FULL PASS: every layer checkpointed, verification clean - Run id 20260928t220203, Modal app id ap-7zxzQj0YqTwlQUP6P06ecn (profile teal-sea) - Source HEAD…
A cartography exercise, not a search. wide_search mined one method, the 10 August 2026 paper More than two thirds of the zeros of the Riemann zeta function lie on the critical line, for a…
Status: a map, not a result. Every computed number below was produced by frontier.py (optimiser shared with wide_search), cross-checked against the paper's closed form where one exists, and…
The height cap on the kernel-checked strip proof is the order-4 Euler-Maclaurin error bar, which grows like a power of the height.
Status: opened. The remainder is not proved.
Status at the time this file was committed: nothing has been computed. The parameters below were fixed first, on the reasoning recorded below, and the commit order is the evidence.
Verdict: VACUOUS. A rival satisfies property 6 in the very box chosen in advance to make that hardest.
Status when this file was committed: nothing has been computed. No zero count, for any function, in any box, had been evaluated when this file landed.
Verdict: VACUOUS. Two of the three preregistered boxes were decided for all four functions, and in both of them all three RH-violating rivals satisfy property 6 exactly as ζ does.
Status when this file was committed: nothing has been computed. The parameters below were fixed before a single truth value was produced.
Status: settled, in the sense that matters, and explicitly not settled in one arm. Nothing here is a result in the repository's sense, and nothing here is evidence for or against RH .
Started 2026-10-03. Route chosen under the 2026-09-12 owner mandate (ALIGNMENT.md section 0), which permits original mathematics toward RH and useful intermediate results.
Nothing here is a result about the Riemann Hypothesis. No zero exclusion, no new bound on zeros, no claim of progress on RH.
id: gauss_positivity-2026-10-03-main hunt: gauss_positivity started: 2026-10-03T09:00-05:00 finished: 2026-10-03T15:30-05:00 ran: - .venv/bin/python hunts/gauss_positivity/newton_battery.py…
Chronological, with the errors kept in. Grades per ALIGNMENT.md section 2: measured is one route at working precision, hardened is two independent routes agreeing, decided is an enclosure…
Question. The sharpest gate in this repository is the quasicrystal gate (zeta/quasicrystal.py, docs/18 §4): the zero measure's Fourier transform is atomic, and the atom pattern detects the…
Status: probe, complete. The quasicrystal lane now has its ground-truth universe: the tapered-transform instrument, pointed at a golden cut-and- project set whose atomic diffraction is…
The lab's Hardy Z development (lean/ZetaLean/HardyZ.lean: hardyZ, hardyZReal, |Z| = |zeta(1/2 + it)|, hardyZReal_zero_iff, continuous_hardyZReal) has been accepted upstream into Mathlib.
2026-10-11. Grade: kernel-checked, in a hunt directory (hunts/README.md: a hunt does not promote its own claim; landing this in the Lean arm is the owner's call).
The initial runs below used one 4-core, 15 GB container, 2026-10-11, times UTC. Lean compiles ran one at a time and never beside the numerics.
Hunt #132 (hunts/hardy_first_zero/, merged as 91848c0c, PR #302) proved in Lean 4 with the pinned Mathlib, zero sorrys and standard axioms only, that riemannZeta (1/2 + tI) = 0 for some t…
2026-10-14. Grade: kernel-checked, in a hunt directory (hunts/README.md: a hunt does not promote its own claim; landing this in the Lean arm is the owner's call).
One 4-core, 15 GB container, 2026-10-14, times UTC. Lean compiles ran one at a time, each after a check that no other lean process was running, and the numerics waited for Lean, with one…
The finite logarithmic mean square is now present in Lean. Its RC2 specialization reduces the remaining coefficient bookkeeping to two explicit endpoint-energy sums.
Half-band update. URMS2-051.md retains the individual log n spacings and the exact two-range coefficient weights in the finite mean square.
The corrected coefficient series is not presently identified with the pair form factor of the zeros of xi'' by the available analytic argument.
The displayed kappa=2 row in Bian Figure 10.1 does not survive independent reconstruction. The first divergence is already
The corrected coefficients define an absolutely convergent power series on |alpha|<=1. In fact, the majorant below has infinite radius.
Status: proposal, not a result. Written from the higher_xi side and aimed at another arm's open step; nothing here is promoted, and the arm it is aimed at owns the decision.
Status: probe record. Two independent derivation chains for the retargeted gate of LEAN-FRONTIER.md item 19, each with every link checked numerically at X = 250 and X = 5000, plus two…
The HigherXi, LogMeanValue, ComplexLogMeanValue, TwoRangeWeights, PowerMargin, MeanSquareAssembly, AristotleRAMS2, and RC2PrefixAssembly modules are the first formal slices of the rebuilt…
Attack the open higher-derivative form-factor problem left by Ji Bian's 2008 thesis and exposed by the August 2026 rank-trace paper.
The source of the elementary x(log x)^2 bound is exact. It is a support overcount, not genuine mass in the level-one resummed coefficient family.
Bandwidth update. BANDWIDTH-FORENSICS.md audits the constants used below. The rho<=1/10 and |alpha|<1/100 values in this report are the first explicit promotion, not final endpoints.
The 0.9544 and 0.9774 proportions on page 93 of Ji Bian's 2008 thesis are chapter-11 calculation errors.
The corrected level-2 coefficient series is now an understood infinite object. The present outcome is split:
This audit closes at Outcome D, current technology barrier.
The old coefficient-tail barrier is closed. CORRECTED-F2.md gives an exact majorant for the infinite corrected series and the uniform bandwidth-one bound
This phase reaches Outcome B: level one repaired, level two blocked.
URMS2-051 survives the independent internal audit.
The strict half-band restriction was created by a worst-frequency-spacing majorant. It is not present in the RC2 Dirichlet polynomial.
This attack closes at Outcome D, resummed barrier sharpened.
Question. zeta/li.py's real-rootedness lane asks about Jensen polynomials J^{d,n}; hunt #4 measured when the de Bruijn–Newman flow lands the Davenport–Heilbronn off-line pairs.
Things that belong to other parts of the tree, recorded here rather than done, because this hunt may not touch zeta/.
Status: probe, complete. Instrument kept; no claim promoted; the headline is a measured dictionary, finite Jensen degree acts on the counterexample's off-line pair as de Bruijn–Newman heat…
Nothing here bears on RH. The Davenport-Heilbronn function satisfies a functional equation of Riemann type and has zeros off the critical line.
Nothing here bears on RH. Every wedge of this shape leaves out n = 0, which is RH itself (MISSION.md, "What success would mean").
Nothing here bears on RH. This file closes, by derivation, the two inputs that RESULTS.md section 12.5 left open in the conditional six-coefficient wedge of hunt
Opened 2026-10-18 as a depth hunt by owner decision: the owner asked for one mechanism worked for weeks rather than a one-day forage. The forage stop rule does not apply here.
Nothing here bears on RH. This file records a bounded literature search, run 2026-10-19, for three results of hunt #135.
Nothing here bears on RH. Phase 0 of hunt #135 reproduces two sign facts from Holland's construction on a finite range of shifts n, and measures one further quantity that phase 1 needs.
Nothing here bears on RH. This file reviews H1_H3.md and RESULTS.md section 16 of hunt #135 as merged on main at 81ce5921 (PR #311).
Nothing here bears on RH. This file reviews RESULTS.md sections 11 and 12 of hunt #135 as merged on main at d0ce271b (PR #308).
Nothing here bears on RH. This file reviews EFFECTIVE.md and RESULTS.md section 18 of hunt #135 as merged on main at 70d72a8e (PR #314).
Every run of this hunt, including the ones whose output was not kept. All runs so far were local and single-core: phase 0 is light by the MISSION's own estimate, and the timing below…
RISK STATUS: CLOSED, and it is a mixed verdict.
Written 2026-08-16, as closure item of GATE.md.
Adjudicated 2026-08-16 (verdict NOT YET, five closure items). Re-adjudicated 2026-08-16 after the repairs, by a session that did not make them. Every field below is at post-repair state.
Written 2026-08-16 to close GATE.md item . The hunt said "two independent winding routes" (MISSION.md WP1, pre-registered prediction P2) and printed that adjective in its headline.
Written 2026-08-16. Vocabulary per MISSION.md: measured is one float route, decided is an enclosure with exact endpoints settling a sign or a containment, cited is somebody else's theorem.
Written 2026-08-18, as task 2 of the pre-submission hardening of hunts/lambda_dh_bounds.
Opened 2026-08-16. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Recorded 2026-08-16, from a web sweep run before the hunt opened. Per the house rule (ontology/knownness.py: an unrun check can never read as absence of prior art), this file says exactly…
Written 2026-08-16. The separation claim Lambda_DH > Lambda_zeta is load-bearing on the exact statement and frame of Polymath 15's upper bound, so both papers are quoted here at source…
Written 2026-08-16, after the gate returned NOT YET with a five-item closure list, and after those repairs were made. This file is the hunt's written record.
Written 2026-08-16, after the gate closed (GATE.md, verdict YES) and after a dedicated novelty adversary attacked the claim's phrasing.
Section draft for WP2 . Instrument: strip.py; decided values in strip_results.json. Vocabulary per MISSION.md: decided means an interval or ball whose exact endpoints settle a sign, stated…
Section draft for the pre-submission hardening of WP2 . Instrument: strip2.py; decided values in strip2_results.json.
Source pinning for WP2 (upper bound) and for the Dobner half-line structure the lower bound leans on.
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking the claim 0.0576 < Lambda_DH <= 0.4006343708899557, not with defending it.
Scratch analysis, 2026-08-16. Remit: break the upper side. Nothing in this file is an enclosure; every number below is measured on one route unless it says otherwise, and the routes are my…
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking 0.0576 < Lambda_DH <= 0.4006343708899557 at the instrument layer, not with defending it.
Scratch analysis, 2026-08-16. Written by an adversary tasked with breaking the novelty of 0.0576 < Lambda_DH <= 0.4006343708899557, not with defending it.
Opened 2026-08-18. Hunt #119 (renumbered from #52 on 2026-09-12). Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Status: OPEN. There is no result here, and this file exists to say so precisely rather than to leave the question to a reader's charity.
Every run this hunt ever performed, including the ones that produced nothing. Reconstructed 2026-09-12 from the committed artifacts and the session record, because the runs that would…
Agent Persona: The Hunter (unsupervised-fun edition) Scope: hunts/lehmer_pair/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md.
Run of 2026-08-07, probe.py, backends 'mpmath.iv', 'python-flint', raw numbers in results.json. Probe language throughout: measured, observed, decided (= an enclosure returned lo > 0 or hi…
Opened 2026-09-10. Nothing in this directory is a result. It is a hunt : exploratory work, recorded before any control has been run against it, and the strongest words it may use are…
Hunt, not a result. Everything below is exploratory . Nothing here is evidence about the Riemann Hypothesis : the Davenport-Heilbronn function is not zeta, has no Euler product, and already…
Every run below happened on one shared container: 4 vCPU, 15 GB, both ball-arithmetic backends live, no Lean.
Opened 2026-10-26, hunt #151, branch hunt/li-dh-onset-hardened. Part of the owner's 2026-10-26 compute sweep: walls the record calls cost walls rather than mathematical ceilings, to be…
Status, 2026-10-26: the pre-registered statement is established at the grade hardened. For the classical Davenport-Heilbronn function:
The box: 32 vCPU, 115 GiB, shared with a campaign pinning Lean jobs. Rules in MISSION.md. Every estimate below was written before the spend it prices.
One documentation defect found in the repository, one new hunt to file, and one process note. Ordered by what needs a decision from you.
Agent Persona: The Hunter (ontology-attempt edition) Scope: hunts/local_positivity/ only. Nothing outside this directory is modified except the case-log entry in hunts/README.md and the…
Paused. No new uniform arithmetic estimate toward RH was established. The controlled norm is standard approximation geometry; the tested update and explicit missing inequality do not make…
The block descent identity survived independent model challenge. The review did not prove RH or the all-scale quantitative decrease.
This continuation keeps prior fixed-prime evidence unchanged. No large pre-existing Nyman-Beurling ladder is run.
Owner-authorized RH research, performed in an isolated worktree from 8941a80. This is one bounded attempt, not a change of the objective to a simple-zero proportion.
Status: ordinary argument with independent model challenge completed. See the review and its limitations. This is not human peer review or a kernel-checked statement.
Disposition: the challenged identities and fixed-P asymptotic survived this review. RH was not established.
Base: 8941a80. Local serial exact arithmetic only. No paid or hosted run.
Checkpoint: oct08-extensions-1. Base: f4ef0715bbe2f4890b3dcea034757ef0c823053a. Owner: Codex root. Isolated checkout, no publication or integration authorized.
Use the repository's installed Python environment (Python3.13 and python-flint0.9.0 were used for Arb checks; the exact DFT producer manifests record Python3.10.4).
Assume QRH: every nontrivial zero of the Riemann zeta function has real part at most 7/8. Then every integer n>=1 has a prime strictly between n^7 and ^7.
Producer documents retain their original pending-review labels and hashes. This file records subsequent review without rewriting those snapshots.
Replace the h+1 central coordinates in the pinned triple network by h coordinates. Retain incidence gather G=B^T, replace scatter by R'c=(Bc-(sum_j c_j)1_v/3)/2, and keep the side maps and…
Owner: dft_audit. Write scope: this directory only. Read source and producer artifacts; no edits there, paid compute, heavy computation, or Git operations.
For each fixed integer h>=22, use the manuscript's triple-indexed network with v=binom, m=h^3, d=binom, W=2v^3+3v^2, Delta=2v^2, and P the least power of two >=W.
Owner: independent dft_audit agent. Write scope: this directory only. Read scope: routes/dft and the pinned manuscript sources.
The public proof at 6b120d1f applies KLN Lemma4.14 and its Table1. No invalid application, incorrect table row, or false density inequality was identified.
Date: 2026-10-08. Independent reviewer: independent_audit.
Claim: If all nontrivial zeros of zeta have real part <=7/8, then every integer n>=1 admits a prime strictly between n^7 and ^7.
Claim: assuming every nontrivial zero of zeta has real part <= 7/8, every integer n >= 1 admits a prime p with n^8 < p < ^8.
Verdict: externally proved in the exact required form. Montgomery and Vaughan, Theorem 12.5, matches the inherited input .
Read-only survey by fresh_opportunities. No repository edits, remote jobs, paid compute, or external messages. Only a subsecond local integer-count sweep.
Checked 2026-10-08. Scope: deleting the dependent total gather from the complex triple network, implementing it with 1/3, and the rank-h lower bound for the unchanged central correction.
Checked 2026-10-08. This is a prior-art assessment, not a proof audit or a priority certificate. No producer proof or computation was changed.
Status: executed bounded research attempt, then rejected in part by coordinator self-review. The route remains open at the generator-to-certificate implication.
Owner class_structure; base f4ef0715bbe2f4890b3dcea034757ef0c823053a. Read-only PR279 3f136908426167ff97888a6ae8b89087223509e6. Write only this directory.
Checkpoint: class-structure-2026-10-08. Owner: delegated class_structure. Read-only repository base f4ef0715bbe2f4890b3dcea034757ef0c823053a.
Before launch: complete odd fundamental discriminants to 20,000, brute-force forms with a<=sqrt; roughly 4,000 small inputs, hard 20-second CPU cap.
Starting with raw ../dft/sources/network.tex at upstream commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb, replace the complex motif's h+1 central coordinates by h coordinates.
Owner: fresh_opportunities; parent coordinates independent audit. Authorized2026-10-08: derive and test removal of the redundant central coordinate in the pinned DFT motif, using exact…
Written derivation, self-review; fresh independent audit pending. No novelty claim. The modification is allowed in the exact-complex-field DFT model.
The h+1 central roles of the published triple motif reduce to h by reconstructing the total sum from the coordinate sums. The new rational scatter preserves arbitrary auxiliary values.
Review the following quantified claim directly from the retained source definitions, before reading the author's PROOF.md or checker.
Verdict: the h=24 result is an optimized instantiation and a formal quantitative corollary of the released construction, not a new Fourier mechanism.
Status: written derivation, self-reviewed; independent audit pending. No novelty or practical runtime claim.
Written result candidate: an h>=22 family replacing a fixed h=100 construction, giving at h=24 an exact-arithmetic DFT bound O(n(log n)^.
Written conditional result, independently audited : assuming every nontrivial zeta zero has real part <=7/8, every integer n>=1 has a prime strictly between n^7 and ^7.
Owner prime_gap_density, 2026-10-08. Read-only lab base and source pins are in MISSION.md. Scope limited to this directory; no Git mutation or paid calls.
Status: written conditional derivation, numerical inequalities enclosed by Arb; independent audit completed in ../../audits/prime-gap/AUDIT.md. No kernel formalization or novelty claim.
2026-10-08, owner prime_gap_density, workspace task-3/routes/prime-gap. Read-only lab f4ef0715bbe2f4890b3dcea034757ef0c823053a, pinned PR276 input 1aff81ebbdb5b749c638a6450016e167f9b3f61e.
Scope: hunts/ontology_provenance/ for the scanner, plus the case-log line, the methods-index entry hunts/README.md requires, and the diagnosis note under hunts/factorization_vs_position/.
provenance.py answers one question about a proposed frame: is anything it reaches zero-derived? It parses the file, classifies the names it uses against a rule set of zero-derived…
id: ontology_provenance-2026-10-27-landing hunt: ontology_provenance started: 2026-10-27T22:50:00Z finished: 2026-10-27T22:58:08Z ran: - python hunts/ontology_provenance/provenance.py…
Opened 2026-09-27 on branch teal-sea/oob-cert from origin/main . Scope: hunts/oob_envelope/ only, plus this hunt's case-log entry in hunts/README.md.
Read first: hunts/oob_envelope/MISSION.md, then AGENTS.md (certainty ladder, compute discipline, reserved words), then arXiv:2608.24827v2 §1–5 and §7.
HOLD after stage B (approved by Thomas 2026-09-27, run, terminal). Stage B: λmin ≥ 5.71789230595e-48 at L = 1.19, T# = 500, N = 500, enclosure-carrying single route, 1.4 core-hours on Modal…
2026-09-28: the L = 0.8 bound and the L = 1.19 stage B bound, both in the even sector, passed independent referee review (referee/REVIEW.md, sections "L = 1.19" and 5).
Every run that costs more than a local 10-minute, 2 GB slot is estimated here before launch. Nothing below has been launched remotely.
Ordinary derivation, self-reviewed, pending independent reproduction. Source checked on 2026-09-28: Zhu, arXiv:2608.24827v2, <https://arxiv.org/html/2608.24827v2>, equations , , , Lemma 6.1…
You are the adversary. You did not write this work and you share no code with it. You are started only when the supervisor has both the theory worker's lemma and modified reduction written…
Authorized by Thomas's 2026-09-27 task, received 2026-09-28. This supersedes only the earlier prohibition on new L=1.19 work. No push or PR. All writes stay under referee/.
Owner: Claude Code referee, branch teal-sea/oob-odd-referee, this checkout only. Thomas approved the follow-up. Commit scoped work, do not push or open a PR without supervisor review.
Frozen before reading the odd worker implementation or its result artifacts. Input revision: 06fdc801d58fe19977dd865134487bfdbf07cecd.
Verdict: PASS, independent odd route and both required controls. Independent L=1.19 endpoint: Q>=2.99e-44 ||f||^2 for real odd f.
Authorized: ODD_BRIEF.md and Thomas's execution request. Incremental Modal input compute cap: 14400 core-seconds.
PASS: independent odd bound >2.99e-44 at L=119/100. Zhu L=4/5, T=150, H=0 validation passes with lower endpoint 7.99e-15. The pole-sign fault and negative-operator control both pass.
1. PASS, independent enclosure: CC-192/Arb proves lambda_min >5.7179e-48 on the full even sector, exceeding both requested and author endpoints. 2.
APPROVED batch completed: 5 successes, 0 failures, 0 inconclusive. Authorization is for these exact five units, sequentially, profile teal-sea, under 20 core-hours and a $0.15 allowance.
Ordinary derivation, self-reviewed, pending independent reproduction. Source checked on 2026-09-28: Zhu, arXiv:2608.24827v2, <https://arxiv.org/html/2608.24827v2>, equations , , , Lemma 6.1…
Frozen before reading the odd worker implementation or its result artifacts. Input revision: 06fdc801d58fe19977dd865134487bfdbf07cecd.
Read first: hunts/oob_envelope/MISSION.md, then AGENTS.md (certainty ladder, reserved words, original vs novel), then arXiv:2608.24827v2 §1–4 and §14–16.
STATUS: holding, no compute. RESULTS.md now cites the referee's final REVIEW.md per result, with no change of ladder grade (every proof stays an ordinary derivation, none kernel-checked).
Branch teal-sea/oob-cert-theory. Author: theory worker (Claude Code, Opus). Every statement below carries its grade on the ladder of AGENTS.md.
Status, 2026-09-06: closed on kill condition 2, at prose grade. RESULTS.md section 8: the out-of-band positivity is worth zero to any certificate whose positivity input is Weil's Hermitian…
Verdict, 2026-09-06: kill condition 2 fires, at prose grade. Section 8 has the argument; sections 1 to 7 are the measurements and the lemma it rests on.
All on the operator's 16 GB Mac, .venv/bin/python, HiGHS through scipy.optimize.linprog. Solve time grows like about X^2.7 in the truncation; the strip adds a few dozen rows and roughly…
Every certificate in the current race reads pair-correlation data on -1,1 and nothing else. The configuration ceiling for that information class is 0.6818286874638, and the whole public…
Verdict: the kill condition did NOT fire, and the hunt found a gap rather than a wall. The unconditional out-of-band positivity of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh…
Estimate written before launching. Two solves were timed first, on this machine: X=40, J=200 took 5.7 s and X=80, J=320 took 40.1 s.
Sixth instance of the ceiling procedure, and the first one aimed at a lower bound. Erdos's minimum overlap constant C. Opened 2026-08-23.
The ceiling procedure on the lower side of Erdos's minimum overlap constant. Run 2026-08-23.
One block per autonomous run. A run that produced nothing records that it produced nothing.
Base: a3acc741396940273ec388548d52752f839593c3.
The paid-shortfall construction has an explicit, fully charged family: truncate a finite balanced seed lift at square-root support.
Planned before the durable run: two seeds, three lift depths, N=2..128 and N=1296, with exact floor/cap checks through 1296. No optimizer, parameter search, random input, or unbounded loop.
This hunt evaluates one finite arithmetic diagnostic at N=144,576,2304,9216,36864. It imports the balanced-prefix cutoff choice from hunts/paid_shortfall_scaling/scaling.py unchanged.
This run used the repository virtual environment. Its reported backends were python-flint, with both mpmath.iv and python-flint available.
Checkpoint paid-scaling-01, base 4efa72ad70a1e535709c33d0eded886d29c19274.
This is an additional proposed refinement from the cap reviewer. It is not a dependency of RESULTS.md or the cutoff-selection algorithm.
Mathematical base: 4efa72ad70a1e535709c33d0eded886d29c19274. This continues paid_shortfall. Its definitions of W_c, B_N, psi, w_q, and C_N^U are unchanged.
Before the first diagnostic: five predetermined cutoffs, 144,576,2304,9216,36864; two coefficient families; two capacities; exact rational algebra; two interval logarithm implementations at…
Base: fd04f1fac9d48a4d769048817e678acdea3b4bdb. Read-only predecessor: af13799d3034b4d6a07e76c0d6a409dc7421f056.
Result: the specified finite feasibility problem is feasible. The vector
Base revision: fd04f1fac9d48a4d769048817e678acdea3b4bdb. The mission was the first tracked file created in this hunt. The checkout was already isolated on its assigned branch.
2026-09-11. Base: ENDPOINT_SHARP.md (commit 367573c, the endpoint checkpoint, unchanged), UPPER_BOUND.md sections 2 to 5, LOCALIZED_MIXED_ENERGY.md section 6, SIEGEL_UNIFORMITY.md .
Independent check, 2026-09-12 (attempt a-0078). Scope: the five items listed in the assignment, covering sections 1, 2 , 3 (major arcs), 4 (minor arcs, including 4.1 in full), and 5 of…
Date: 2026-09-20 (revised following independent review). Base commit: 271fc26. Prior work: FRONTIER_2026_09_12.md, SIGNED_MEAN_RENEWAL.md, FRONTIER_INDEPENDENT_REVIEW.md…
Date: 2026-09-20. Reviewer: Muse worker (Grok unavailable; this package covers both the mathematical challenge and the independent diagnostic).
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. This is the next arithmetic estimate for the original CHHL total error.
- Artifact: THEOREM_B_FORMULA_REPAIR.md, with formula_repair_checks.py and results_formula_repair_checks.json. - Reviewed form: 95ae36b9c09c0cf28844e40e50f7fceac2f95cfb.
2026-09-10. Builds on CORRECTED_RH_BRIDGE.md, LOCALIZED_MIXED_ENERGY.md and EXCEPTIONAL_ENERGY.md as they stand on this branch.
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. PRs #209 and #210 are completed, separate attempts and are unchanged.
2026-09-10. Target: CANDIDATE_ENERGY.md as it stands on this branch, which claims not just the requested domination \(E{\rm corr} but the exact identity \ E{\rm corr}\qquad\text{for every…
2026-09-09. Base: PR #213 at 284a52fbb369f48fe011578bc7e0299b23b5bce0. The records in PRs #209-#213 and the completed literature comparison are unchanged.
This is the coordinator's candidate argument in the exact mathematical version reviewed on 2026-09-09. It had no endpoint commit when reviewed.
The coordinator supplied the candidate argument directly in the Codex review request on 2026-09-09. At review time it had no endpoint commit or attached file.
Correction notice, 2026-09-11. Section 2.3's conclusion that no choice of the Bonferroni cutoff \ works at \ does not hold.
2026-09-11, corrected the same day in three revisions (sections 2 and 4; every correction is recorded in place below rather than silently applied: the Mertens estimate in section 2, the…
Independent check, 2026-09-11. Read in order: ENDPOINT_SHARP.md, ENDPOINT_BOUND.md (section 2 and equations , , , , , , ENDPOINT_HALF.md (including its correction notice), and…
Independent check, 2026-09-11 (attempt a-0077). Scope: only the two substitutions of section 4 (the progression input and the separate sieve level \, which postdate ENDPOINT_SHARP_REVIEW.md…
2026-09-09. Continuation of PR #212 at 76ed1155d087d9137306d3632f66dba7555aadc3. SIEGEL_UNIFORMITY.md and the completed records in PRs #209-#211 are unchanged.
This document records the constructive next step in the arithmetic investigation of $D_N$, the defined signed prime-counting functional.
2026-09-12. Base: science commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb. Review status is recorded in FRONTIER_INDEPENDENT_REVIEW.md.
Date: 2026-09-20. Runtime observed: Gemini 3.8 Flash high (provenance accurately recorded; not Opus, per coordinator notice).
2026-09-09. Base #215 at 3645324cf69497e197592fdcc2f630c4ed6504b0. Working record only. No research PR or push: this mechanism fails to improve the complete bound. #209-#215 are unchanged.
2026-09-12. Continuation from science commit 3b0fc2e3 and the separately recorded board/history at 88b5d1a5. Earlier work is preserved.
Date: 2026-09-12. Source base: zeta-lab commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb.
2026-09-09. Base: #214 at cb0189db3863ac43b2314c7df1008636bd4da477. The accepted bridge and #209-#214 are unchanged.
2026-09-12. Base: ARC_SPLIT_BUDGET.md (commit a537765; its arcs, its minor-arc bound and its budget are reused unchanged), ENDPOINT_SHARP.md sections 1, 4 and 5 (the model at \, the…
2026-09-12, attempt a-0080. Scripts written fresh for this review, not reusing major_arc_explicit_probe.py: major_arc_explicit_independent_check.py (item 1) and…
2026-09-08. Continuation from UPPER_BOUND.md at 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. This is one attempted replacement of the minor-arc supremum estimate: retain the amplitude…
Chou, Haag, Huryn and Ledoan (arXiv:2308.14888, J. Number Theory 2025) define, for the von Mangoldt pair count psi_2(N, k) = sum{n, n' <= N, n' - n = k} Lambda Lambda and the…
Base: b8bb28c4de357827be0bdad95a5e9b40d9c4e669 (author file at 3d5c666634766357e2c6484afb0e6fbd4c8f2540; review at §7 repair spec incorporated 2026-09-20). Date: 2026-09-20.
- Target: hunts/prime_pair_error/MOBIUS_PAIRING.md - Base Commit: 425e4f46355c1f68bce3ed064b818de7f265feb3 (repair of prior review dispatch; author files remain strictly read-only at…
2026-09-12. Base: SHARP_EXPONENT.md (commit 3b0fc2e, the two-sided statement and its budget , MAJOR_ARC_EXPLICIT.md (its sections 2, 3 and 5, the lemma , the case analysis of section 3 and…
2026-09-10. Builds on CORRECTED_RH_BRIDGE.md, SIEGEL_UNIFORMITY.md and LOCALIZED_MIXED_ENERGY.md as they stand on this branch, and directly answers the question CANDIDATE_ENERGY.md left…
This document answers one question, precisely scoped: RANK3_ROUTE_D.md §6 shows that the direct, per-arc transfer bound used in its equation — the generalization of UPPER_BOUND.md's from \…
This document checks, against citable primary sources rather than by re-derivation, a specific hypothesis H that would be needed to push RANK3_MEAN_VALUE_TOOLS.md Section 3's…
This document answers the task assigned to it: whether RANK3_CROSS_TERM_CANCELLATION.md's identity \, proved there only for prime \, extends to composite squarefree \ with \ distinct prime…
2026-09-11. This document finishes the estimate that RANK3_COMPOSITE_CROSS_TERM.md section 5 left as its one remaining step: carry the exact conductor-weighted identity over the complete…
This document answers the task assigned to it: whether \(\Sigma{\rm cross} in RANK3_ROUTE_D.md's exact identity can be proven, not merely assumed or measured, to be small relative to…
RANK3_ROUTE_D.md's exact identity splits the coprime-driven part of \, summed over the reduced residues \(a\bmod q\), into a diagonal piece \(\Sigma{\rm diag} and a cross term \ \Sigma{\rm…
This document answers the question RANK3_MEAN_VALUE_TOOLS.md Section 5 and RANK3_BDH_VERIFY.md leave open: does an "integrated" Barban-Davenport- Halberstam-type theorem exist, or can one…
This document investigates, as RANK3_SCOPE.md Section 2 asks, whether some unconditional tool other than the three named in UPPER_BOUND.md -- the Siegel-Walfisz major-arc approximation…
This is an investigation, not a proof attempt, of one sub-question RANK3_SCOPE.md leaves open. RANK3_SCOPE.md Section 2 shows that none of the three tools UPPER_BOUND.md assembles…
This document answers the task assigned to it: search the unconditional analytic number theory literature for a "t-integrated" analogue of the Barban-Davenport-Halberstam /…
Scope and a note on method. This document answers the literature question RANK3_QUARTIC_TOOLS.md Section 3 leaves open (its own "wall"): is there a named, unconditional theorem bounding \…
Scope and relation to prior documents. This document's task is the one RANK3_QUARTIC_TOOLS.md closes with as unfinished (its §4, "What would settle this precisely"): search further for a…
A note on sources. This attempt's assignment describes a file RANK3_TOOLS.md (Section 3: a second-moment identity for \, which does not apply to \, verified in rank3_identity_check.py) and…
RANK3_SCOPE.md's Route A asks for an unconditional, uniform-in-\ estimate for \, strong enough to make \ S^2\sum{b\bmod q}^T, \qquad T^2, \tag{S}\ for \(R_0=\lfloor Q/L\rfloor\)…
This document carries out RANK3_SCOPE.md's Route D: the exact analogue, for general modulus \ and reduced residue \(a\bmod q\), of UPPER_BOUND.md's Parseval identity and its arc-transfer…
This is a scoping document, not a proof attempt. It does not estimate the quantities below; it says precisely what they are, why UPPER_BOUND.md leaves them unestimated, what closing them…
2026-09-11, corrected the same day (section 4 rewritten around a cited theorem; the first version carried a reversed density-exponent condition and an overstated zero-free-region saving…
This is a preservation record, not a new mathematical result or a change of research assignment. The current prime-pair continuation remains FRONTIER_2026_09_12.md, with its independent…
Editorial note, 2026-09-06: the absolute path of the reviewer's worktree was replaced with "an isolated local worktree" to satisfy tests/test_repo_hygiene.py, which bars machine-local paths…
All numbers below are in results.json, written by probe.py on 2026-09-06 (run cost in RUNS.md). Notation as in Chou, Haag, Huryn, Ledoan : psi_2(N, k) is the von Mangoldt pair count with…
Estimate written before the large run. decompose at N = 10^6 took 1.2 s and the whole script 3.1 s; the FFT is N log N, so 10^7 was priced at about 15 to 20 s for the decomposition plus the…
2026-09-10. Reuses probe.py's FFT-autocorrelation route for \ unchanged, and the character/sieve helpers in artifacts/siegel_uniformity/check.py for \.
2026-09-10. Builds on CANDIDATE_ENERGY.md, CORRECTED_RH_BRIDGE.md, LOCALIZED_MIXED_ENERGY.md and ENDPOINT_BOUND.md as they stand on this branch.
Frontier correction, 2026-09-12. The negative conclusion of section 1.2 is withdrawn. Its AP-variance calculation omitted the centered principal character, undercounted induced characters…
2026-09-12, attempt a-0082. Two scripts written fresh for this review, not reusing sharp_exponent_probe.py: review_a0082_sharp_exponent_check.py (numerical checks of section 5's two items…
2026-09-09. Base: 2da62eb9842db72d4f6bad09c6f13efe384d6ab7. The completed attempts in PRs #209-#211 are unchanged.
Base: zeta-lab commit 3b0fc2e3c97b46cc1fde6af0ff3dd856898d95fb. Date: 2026-09-12. Handwritten derivations for independent review; no novelty claim.
delta_sq_sw_bind.py evaluates Section 7's proved statement \^2\ll_H N^3L^{-2H}\) (\(L=\log N\)) under an explicit, labeled convention -- assumed implied constant \ -- because the proof…
This checks one specific question: can the Siegel-Walfisz major-arc argument of UPPER_BOUND.md Section 5, equations — proved uniformly for denominators \(q\le Q'=\lfloor L^B\rfloor\), any…
This is a derivation check on a polylog-sized range of denominators, not a proof attempt and not a claim about RH.
Status: useful intermediate lemma with exact hypotheses, plus a conditional strengthening of Theorem B. Grade: measured and derived, with hypotheses stated.
- Artifact: hunts/prime_pair_error/THEOREM_B_FORMULA_REPAIR.md (+ formula_repair_checks.py, results_formula_repair_checks.json) - Reviewed SHA: 95ae36b9c09c0cf28844e40e50f7fceac2f95cfb…
Scope correction, 2026-09-12. The proposed absolutely convergent zero expansion in section 3 is not established: its coefficient \ decays as \, not its square.
2026-09-06. This attempt obtains \ E\ll_C N^3(\log N)^{-C}\qquad\text{for every fixed }C>0, \tag{1} \ unconditionally, for all sufficiently large integer \, with ineffective constants.
Opened 2026-08-18. Hunt #119 (renumbered from #52 on 2026-09-12). Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Status: OPEN. There is no result here, and this file exists to say so precisely rather than to leave the question to a reader's charity.
Every run this hunt ever performed, including the ones that produced nothing. Reconstructed 2026-09-12 from the committed artifacts and the session record, because the runs that would…
2026-09-06. This is an attempted proof mechanism, its failure analysis, and a constructive stress test.
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: mathematical proof draft with executed finite/symbolic checks. No independent referee review, formal verification, novelty claim, or improved bound on total E is…
This file records the complete research lineage that led to the frontier drafts in this directory.
This directory preserves the frontier work produced during the 2026-09-06 continuation of hunts/prime_pair_error before the next agent phase.
Date: 2026-09-06. Status: self-contained written proof draft, with an executed finite checker. No independent referee, novelty claim, formal verification, or improvement to the total…
Continuation of the 2026-09-06 factorial-certificate investigation.
Snapshot ID zeta-adaptive-freeze-v1. This directory is storage. Thomas paused the research and asked for the evidence to be preserved; nothing here was reviewed, promoted or extended by the…
Thomas has paused the research. Finish one clean repository checkpoint, then stop. Do not resume mathematical exploration in this task.
Snapshot ID: zeta-adaptive-freeze-v1 Research lineage: continuation of the 2026-09-06 Zeta Lab investigation.
A preservation checkpoint through the adaptive 23-correction block. Read FREEZE.md for the detailed claim/status ledger and the exact unresolved question.
Session 2026-09-07. Companion to RESULTS.md. Everything in Sections 1 and 2 is proved (elementary, finite, checkable by barrier_lemmas.py and tests/test_certificate_lp_barrier.py).
Session 2026-09-07 . Input: main 880ec07. Scope: the attainable-quotient problem T of hunts/quotient_certificate/RESULTS.md (PR #203), kept separate from the all-cell problem V.
Question. For support bound y and cutoff N, what is the smallest excess B - psi any factorial certificate can have?
Correction and continuation, 2026-09-07: Section 4.2's dimension-count argument is false: N=27,y=9 has eight constrained cells but minimum excess log, by an exact row relation and attaining…
All on a 16 GB M4 laptop under a foreign load average of 60 to 140 from another session's agent fleet, so wall times are inflated several-fold.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Reviewer: a Claude Code session working from the repository, not the session that produced the package.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: elementary deduction plus two computed seed instances, checked by exact integer arithmetic and rational logarithm enclosures.
Snapshot date: 2026-09-06. Purpose: preserve and document the existing record, not begin another mathematical pass.
2026-09-06. Preservation only; no new mathematical result or agent run.
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06. Status: elementary deduction plus two computed seed instances, checked by exact integer arithmetic and rational logarithm enclosures.
Date: 2026-09-06. Executed in this chat. Not committed to Zeta Lab.
Reviewed 2026-09-06, in a fresh worktree, by a session that did not write the pilot.
Comparison, 2026-09-06, the third objective on the pilot's seed family. It is separate from ../factorial_full_cost/, whose record and conclusions are left unchanged, and from the preserved…
Experiment, 2026-09-06, a follow-up to the preserved pilot in ../factorial_certificate_pilot/ (read PILOT.md, pilot.py and REVIEW.md there first).
Date: 2026-09-06.
Date: 2026-09-06. Reviewer: a Claude Code session working from the repository, not the session that produced the candidate.
Date: 2026-09-06 (local investigation date).
Date: 2026-09-06. Status: written derivation with executed exact arithmetic checks. This is not an independently reviewed theorem, a novelty claim, an improvement over established…
Date: 2026-09-06. Prepared in this conversation.
Date: 2026-09-06.
Date: 2026-09-06, local conversation date. A continuation of the saved joint-support analysis.
Status: drafted 2026-08-16, not posted. Posting is an operator action; this hunt may not open issues on its own behalf, and this file is the artifact, not the act.
Opened 2026-08-16. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
DRAFT. Nothing in this file has been posted. Posting to OEIS is an operator action, explicitly outside this hunt's permissions (MISSION.md, agents_may_not).
Written 2026-08-16, after an adjudication that the prior art owns the core of this hunt. The verdict is settled and this file does not relitigate it.
Run of 2026-08-16. Instruments: decide.py and theorem_inputs.py (decided constants), controls.py , witness.py ; raw numbers in decided.json, theorem_inputs.json, controls_results.json…
This file pins the texts the hunt attacks and the literature it leans on, so that every later step works against the served words rather than a paraphrase.
Hunt: prime_zeta_rightmost. Written 2026-08-16. This file states and proves the replacement for the two conjectures in OEIS A107311, against the verbatim text pinned in SOURCE.md section 2.
Base commit: ef4e0564 . Branch hunt/qrh-class-number. Status: bounded construction on top of an unreviewed input theorem.
Status: candidate, pending external review. Every statement below is proved, given OpenAI's Theorem 1.1 (input theorem below, unreviewed).
Checkout /home/user/zeta-lab-qrh-class-number, branch hunt/qrh-class-number from origin/main at ef4e0564. zeta.rigor.BACKEND is python-flint (backends 'mpmath.iv', 'python-flint').
Opened 2026-10-08. Hunt #121. Nothing in this directory is a result until the case log in hunts/README.md says how it ended, and even then nothing here is evidence about RH: every statement…
Grades used: derived (an ordinary argument on the cited inputs, written out below, reviewed by nobody), measured (one mpmath route, dps 30, pinned by test_qrh_conditional.py), cited…
Estimate written before the run. Section A is exact rational arithmetic . Section B scans two functions of one variable on a grid of pitch 1/4 over log 2, 5000, 20,000 evaluations each, at…
Base commit: ef4e0564349c19c9e6ca91e78ebe3e4f5e224997, branch hunt/qrh-linnik. Opened 2026-10-08.
Status: candidate, pending external review. Grade of every theorem below: proved (ordinary written proof, written by a model in this hunt, not yet reviewed by anyone), given OpenAI's…
Worktree /home/user/zeta-lab-qrh-linnik, branch hunt/qrh-linnik, from origin/main at ef4e0564349c19c9e6ca91e78ebe3e4f5e224997.
Base commit: ef4e0564 . Branch hunt/qrh-nonresidue.
Status: candidate, pending external review. Every theorem below is proved, given OpenAI, "The Quasi-Riemann Hypothesis", Sept 30 2026, Thm 1.1 (zero-free half-plane Re s > 7/8 for every…
Checkout /home/user/zeta-lab-qrh-nonresidue, branch hunt/qrh-nonresidue from origin/main ef4e0564. zeta.rigor.BACKEND reported python-flint with both backends available; python-flint 0.9.0.
Base commit: ef4e0564 , branch hunt/qrh-prime-powers. Status: construction hunt. Its claims are candidates pending external review.
Status: candidate, pending external review. Every statement below is conditional on OpenAI's zero-free half-plane and is "proved, given OpenAI's Theorem 1.1" in the following sense: the…
Worktree /home/user/zeta-lab-qrh-prime-powers, branch hunt/qrh-prime-powers from origin/main ef4e0564.
Opened 2026-10-08. Hunt #120. Nothing in this directory is a result until the case log in hunts/README.md says how it ended.
Hunt #120, 2026-10-08. Status: measured and read; nothing here is evidence about the truth of the paper's theorem.
Every run, including the ones that produced nothing. Wall times are from a four-core cloud container, one process per core; nothing ran on the operator's machines.
Continuation of PR #207 from 02e6780. The consumed definition is Fable's PR #208, Section 8 and fold_family.py at f4ae24f027f07916037ca8fe6c56c95a29cbf4d7.
Continue PR #207 from 02e6780d6c81e91d5151f93a89fb14ec13664cca. Consume Fable's latest fold definition from PR #208 at f4ae24f027f07916037ca8fe6c56c95a29cbf4d7, especially Section 8 and…
Continuation of PR #207 from d79fe15. The other lane's current input is PR #208, Section 9 at 0eb39186334612b3e55db315758c49ab87a29763, including Rule C and its reported failure at cell 33.
Continue PR #207 from d79fe15ae0feabf0f0529332526e1812e16e0312. Consume Rule C in Fable's PR #208 at 0eb39186334612b3e55db315758c49ab87a29763 without editing its files.
Input: 880ec07ae605d93f4c49e4464d8b4526457cfb65. This is a continuation after #203, #205 and #206, preserving their artifacts and corrections.
Input: main 880ec07ae605d93f4c49e4464d8b4526457cfb65, after PRs
Continuation of PR #207 from cce45bd. The rational upper certificate is supplied by the coordinator and recorded in fold_upper_input.json.
Continue PR #207 from cce45bd2bb3a9c1715ef2d4ad6269481dda5ed42. Input comparison: Fable's PR #208 at a343fed9b396bfa32b7f415576842e8c051458b5. Leave both PRs open.
Continuation of PR #207 from 3099c7a. The consumed input from Fable's PR #208 is pinned at 600ff8044ed9f5e30b9dd9ddc5f488faf1af329a. Both PRs remain open.
Continue PR #207 from 3099c7ac01eeeb1542bf40478fd73d1d58e794d3. The coordinator selected the class with N>=10000, y=floor, coverage on every Q_N cell and B_c<=2N.
Continue the factorial-certificate investigation from main d393e1a. The previous LP imposes positivity at every integer cell through N, although its prime sum evaluates the certificate only…
2026-09-07. Three finite ceilings improve after dropping constraints at unattainable cells. Rational coefficients satisfy every retained constraint in exact integer arithmetic.
Input baseline: main d393e1a, GitHub Actions tests run 34088036566 and checks run 34088036541 both passed.
Continuation of PR #207 from 45b3d9b. The construction consumed here is Fable's PR #208, Section 6, pinned at 3d8aa03034d5207cdab3129eb78534c0f77d2384.
Continue PR #207 from 45b3d9b2625dcf7695a7fbc811e3e2678af6fb27. The height-kernel assignment is complete; do not minimize variance.
An adversarial audit by a separate agent with no part in producing the result, given the write-up and the repository and told to break the claim rather than review it. Fifteen attacks.
hunts/prime_pair_error/frontier/2026-09-06/certificate_lp_frontier/RESULTS.md section 4.6 reports the attainable-quotient floor T(y, N) - psi at four cutoffs, all on the diagonal y =…
2026-09-10. Grade: measured (floating LP, HiGHS dual simplex), with every optimum recomputed from the returned coefficients through the constraint definition.
id: quotient_exponent-2026-09-09-reformulation hunt: quotient_exponent started: 2026-09-09T23:15-05:00 finished: 2026-09-10T00:05-05:00 ran: - OPENBLAS_NUM_THREADS=1 .venv/bin/python…
Two runs. Run 1 (16585a2a-04a0-4eda-925f-1a79df23d758, branch hunt/r-0339c1, budget 60 minutes) proved the Chebyshev half and the double-counting first step, and named the wall: Mathlib has…
Outcome: settled. The Hardy–Ramanujan theorem is proved, kernel-checked with zero sorrys: ZetaLean.HardyRamanujan.hardy_ramanujan establishes the density form of Turán's argument, with…
tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word is the guard that keeps hunts/ from claiming the word zeta/rigor.py owns.
Status: settled. The guard's boundary is a case-insensitive match on one literal substring. Everything outside that substring passes, including the four words the repository's own…
The previous census proved that the choices of one supported monochromatic perfect matching in each of three colours fall into 31 orbits. That does not quotient the full polynomial system.
Status: exact support census settled; algebraic sieve open. No 8x3 branch has been closed and no complex witness has been found.
id: r_044dd2-pilot hunt: r_044dd2 started: 2026-08-22T00:15:38-05:00 finished: 2026-08-22T00:18:35-05:00 ran: - orbit 0 with repeated bounded support minimization and 48 lazy cuts per round…
harness.review.standing_reasons returns, for the claim urms2-0.51 in harness/departments/review_ledger.py:
Outcome: the attack ran, the claim is not withdrawn, and it found three things about the record that a reader leaning on this claim should know.
Second instance of the reproduction procedure outside mathematics, paired with issue #140 (soundcalc / zkVM).
Read 2026-08-24. SWE-bench/experiments pinned at commit 1faa91cade0562ba62b66c1c99e71f7b72d96f13; split ids from princeton-nlp/SWE-bench_Verified at dataset sha…
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
lean/ZetaLean/HardyRamanujantheorem.lean landed the Hardy–Ramanujan theorem in its density form, with zero sorrys, on top of ZetaLean.Mertens.mertens_second_theorem.
Status: settled. Both threads closed, zero sorrys, axioms unchanged, no statement weakened.
Question. hunts/frontier_math/o9_leaf.py states a LEAF CAVEAT: its transcendental leaves come from Arb at 300 bits rounded outward with a 4-ulp pad, BandCert/Leaves.lean builds them from…
Settled. Issue #23's claim holds, and the outstanding item it named now has a number. o9_leaf.py's LEAF CAVEAT is false as a safety argument, its 344 is low by 38%, and the corrected 1-D…
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Question. Does scripts/make_context.py --check detect public functions added under meta/, and what is the exact boundary of this blind region?
DeepMind's alphaevolve_repository_of_problems marks Problem 42 (the sum-difference problem) world_record in status.json.
Verdict: option 1 of the three the brief names. Penman and Wells reach a strictly higher value of exactly the quantity DeepMind's Problem 42 defines, and they do it with an explicit finite…
Two directories in this laboratory carry a table of the same quantity and disagree from i = 2 onward, with conflicting diagnoses of why:
Verdict: settled. An independent recomputation, written for this adjudication and importing neither disputant, reproduces hunts/higher_xi/C2_EXACT.json exactly at all eleven indices, and…
CONTINUATION of R-322DAE Source: operator Reference: prize:krenn-gu:n8-d3-orbit-reduced-system
The 6x3 system was evaluated on the 8-variable H x S2 quotient. Groebner basis completed in 0.44s and returned 1, confirming the no-complex-witness verdict.
The 3000 euro Krenn-Gu conjecture asks whether there exists an edge-weighted graph whose monochromatic matching polynomial satisfies specific quantum interference conditions.
This hunt settles the orbit-census layer for the Krenn-Gu 8x3 instance ($n=8$ vertices, $d=3$ colors).
tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word is the lexical guard that scans hunts/ to ensure probe files do not claim the certainty regime reserved for…
Status: settled. The guard tests/test_hunt_probe_discipline.py::test_no_hunt_claims_the_reserved_word enforces an explicit suffix whitelist: path.suffix.lower() in {".py", ".md", ".json"}.
Mathlib's wanted-theorems tracking records Mertens's theorems (Wikidata Q1196729) as wanted and unbuilt.
Continuation run 05c755d3-1e75-4596-98b3-34ca2c084175, building on run ed50af7f (Hunt #30), which landed the first theorem and route-mapped the second.
One new file, lean/ZetaLean/Mertensstheorems.lean (409 lines), plus its import line in lean/ZetaLean.lean.
hunts/frontier_math/k2_closure.py::zone_trade maximises, over integer zone multiplicities with sum m <= 10, the adversary's zone trade
2026-08-17. Hunt r_401bbf, run 2b9b08aa. Instrument: probe.py, data: results.json, pins: test_prune_discharge.py. Reads: hunts/frontier_math/k2_closure.py, hunts/r_a97060/RESULTS.md §4.
harness/departments/guard_ledger.py carries the guard scripts/make_context.py --check with fired=None, known_misses=() and scope="undetermined until demonstrated".
Question. Does scripts/make_context.py --check catch its declared smallest mutant, and where does its sensitivity stop?
Source: teal-sea/zeta-lab issue #140. Started 2026-08-24.
Read 2026-08-24. ethereum/soundcalc pinned at commit d9078d64c9c3ae15b0931f6d249b2dc073194f15 . Vendor sources read at the commits and tags the TOMLs name, and again at each vendor's…
ZetaLean.HardyRamanujan.sum_sq_dev_le carries Turan's variance bound with the explicit constant 5855.
Settled. The variance constant moved from 5855 to 275, a factor of 21.3, with every statement's shape preserved, no hypothesis added, no sorry, and a green lake build.
Date: 2026-08-22
Target repo: teal-sea/zeta-lab · Branch: hunt/r-662b12 Source: operator · Reference: prize:aimo-interpretability-2026:baseline Task ID: 31e8a4f2-2c99-4bb6-953c-63f332cc07c4
Target repo: teal-sea/zeta-lab · Branch: hunt/r-662b12 Task reference: prize:aimo-interpretability-2026:baseline Telemetry Run ID: 31e8a4f2-2c99-4bb6-953c-63f332cc07c4
Run 4df2ee65-1c9a-4e3b-8f7d-2a6b9c4e0f11, branch hunt/r-6c7d6a-4df2ee65, budget 75 minutes, no operator supervision.
Run 4df2ee65-1c9a-4e3b-8f7d-2a6b9c4e0f11, 2026-08-17. Target: the numerator-side boxParts fields of the O9 two-dimensional checker, in hunts/frontier_math/zeta23ext/Zeta23Ext/EForm3/.
Run bc87fba6-95d1-4ce0-a9ef-c7e364c95bcb, branch hunt/r-6f088d-bc87fba6, budget 30 minutes, no operator supervision.
Run bc87fba6-95d1-4ce0-a9ef-c7e364c95bcb, 2026-08-18. Hunt #49.
Fourth instance of the lab's ceiling procedure (issue #110: reproduce a published certificate, read its verifier for soundness, measure where the method's own ceiling is, then push the…
Everything below is float grade (rung 1, "measured"). No interval arithmetic is used anywhere in probe.py, so no statement here climbs past measured except where it reproduces a value that…
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Question. Does scripts/make_context.py --check detect in-place length-neutral private helper renames in modules with all, and what is the exact boundary?
Fifth instance of the ceiling procedure: convex-program certificates for Erdos's minimum overlap problem. Opened from issue #111, run 2026-08-23, budget 30 minutes, no operator supervision.
Fifth instance of the ceiling procedure: convex-program certificates for Erdos's minimum overlap problem (issue #111. Run f0bbb14a-833d-456a-befa-2e4f74ba6947, 2026-08-23, budget 30 minutes.
DeepMind's AlphaEvolve mathematics report claims C_3 <= 1.4557 for the "third autocorrelation inequality", improving a prior 1.4581.
Run 9698c990-e812-4890-94d8-f30a65b820af, 2026-08-23. Issue teal-sea/zeta-lab#123. Reproduce with python3 hunts/r_8539dc/probe.py (standard library only).
Run: 40c2efbc-2ed1-4de3-a762-fc57524791f6 · Case log: Hunt #47
Both halves landed, zero sorrys, standard axioms only. The two dead-weight seam lemmas are retired at no reproof cost, and the two-mode arithmetic is proved and instantiated at a recorded…
This is a mapping run, not a proving run. It buys coordinates. It does not attempt Erdős–Kac and it must not: starting to prove the theorem is a declared kill condition, not a stretch goal.
Status: settled. Both routes are mapped, both are priced, and they are not close. The moment method is roughly 2,400 to 3,700 lines of Lean and every one of its obligations is a thing…
docs/25 §4.3 defect 2 and commit 44d3133 record the same defect from two sides. The rung-3 grid sites carry a pred_beta drawn from mpmath point evaluations at the achievable bound, so the…
Status: settled, with one prediction in docs/25 refuted.
Run bbe76b9a-ccf3-4d53-bfe9-6480334f4648, opened 2026-08-17.
Run bbe76b9a-ccf3-4d53-bfe9-6480334f4648, 2026-08-17. Hunt #44.
hunts/frontier_math/K2-TWO-SPECIES.md section 2 records a depth-extended landscape table whose last row is starred as a correction:
2026-08-23. Run e09a7f8a. Reads: hunts/frontier_math/K2-TWO-SPECIES.md section 2, two_species.py, Zeta23Ext/EForm3/FarField.lean, Zeta23Ext/EForm3/Counting.lean.
hunts/frontier_math/k2_closure.py closes the k = 2, equal-depth case of blocker 2 over 6600 tau-cells on 0,132, and closes it at measured grade: every supremum in that table is a…
2026-08-17. Hunt r_a97060, run 78b4ce8e. Instrument: probe.py (+ ball_field.py), data: results.json. Reads: K2-TWO-SPECIES.md §3 and §6, hunts/frontier_math/k2_closure.py.
- Target: teal-sea/zeta-lab - Branch: hunt/r-abf47b - Budget: 60 minutes - Goal: Run exact ideal membership / Groebner basis on the Support-7 restricted system (138 variables).
The 6x3 system was evaluated on the 8-variable H x S2 quotient. Groebner basis completed in 0.16s and returned 1, confirming the no-complex-witness verdict.
- Installed from hunts/r_044dd2/requirements-solver.txt successfully. - Re-ran hunts/r_044dd2/audit.py on artifacts/orbit18-support-07.json: Passed (verified_support_survivor: true).
The run kept no ledger. The first three entries reconstruct its computations on landing from RESULTS.md, results.json and HANDBACK.json; their start and finish times were not recorded.
Opened 2026-08-18.
The question investigated is whether the first positivity failure of the Connes–van Suijlekom / Connes–Consani–Moscovici Galerkin truncation of the Weil quadratic form on the…
Run 37fb06a9-44a6-42d5-abc3-4c1342b1287b, 2026-08-18. Reads hunts/frontier_math/K2-TWO-SPECIES.md (section 5, the T1/T2 split), hunts/frontier_math/two_species.py…
Hunt r_b9552d, run 37fb06a9-44a6-42d5-abc3-4c1342b1287b, 2026-08-18. Instrument: probe.py (runs end to end in ~6 minutes; --quick in ~10 s). Data: results.json.
Hunt r_b9552d, run 2, run id 113786a8-1f1c-4220-b772-15160a0274fa, 2026-08-20. Instrument: probe.py (--quick in seconds, full in a few minutes). Data: results.json (and results_quick.json).
harness/departments/guard_ledger.py records the guard scripts/make_context.py --check with the known miss:
Status: settled. The guard scripts/make_context.py --check does not detect test files whose names do not match test.py (such as tests/mutant_helper.py, tests/conftest.py, or…
harness/departments/guard_ledger.py records the guard tests/test_docs_numbering.py::test_no_two_docs_share_a_number with the known miss:
Status: settled. The guard tests/test_docs_numbering.py::test_no_two_docs_share_a_number does not detect a document renamed without its number changing when citations use bare references…
Run 872d7dce-5f49-4e7c-8fcf-f470fd066e6f, opened 2026-08-24. Parent: hunts/r_b9552d run 37fb06a9 (RESULTS-37fb06a9.md §5, loose thread 2), which recorded the route as assessed and not…
harness/departments/guard_ledger.py carries this record:
Status: settled, at the level a mutation battery can settle it. Ten mutants built, ten run, one null control.
Question. Does scripts/make_context.py --check detect public functions, classes, constants, or module additions under compiler/, and what is the exact sensitivity boundary?
Question. Does scripts/make_context.py --check detect public functions, classes, constants, or module additions under compiler/, and what is the exact sensitivity boundary?
A standing limitation on every claim compiler/ makes. Recording it publicly because it bounds what those verdicts mean.
This hunt establishes, measures, and records the exact scope caveats bounding all claims made by the compiler/ department.
claude/riemann-hypothesis-research-ofds8s ran a wide-portfolio RH-adjacent campaign on 2026-08-17/18 and never landed.
Status: settled. Four arms landed, one held back on purpose, 29/29 acceptance checks pass, and one real defect was found in the material while checking it.
Publishes the artifact queued by issue #21: a partial computation established that three commonly-cited structural properties of ζ are satisfied by every RH-violating look-alike in…
Status: settled for the five properties issue #21 queued; the sixth was already settled by earlier hunts in this tree, and what this run adds to it is the number that says why it is…
claim 'urms2-0.51' has no recorded blind attack: the review is not standing until one runs
What modification of the world would preserve the appearance of this result while making its interpretation false?
Test AGY conversation context and handback 8.
Status: settled.
Inspection base: 6a9aa8fd4074ea23868c1c547168c0c773185781, fetched on 2026-09-04. This is a map of inspected interfaces and selected proofs, not an audit of every theorem in the repository.
Opened 2026-09-04 at repository commit 6a9aa8fd4074ea23868c1c547168c0c773185781 following the operator's request for a whole-laboratory structural research experiment.
Recorded 2026-09-05 and committed 2026-09-14. Continuation from 1c4625b04 (the counting audit commit). Status: research proposal.
Status: candidate refuted at the stated scope (ALIGNMENT.md section 5, disposition 1). The refuted claims are hunts/amtopa_ceiling's recorded lower endpoint 0.007916857810 and its target…
Manifests for the runs this hunt reports. The session that did the work on 2026-09-04 wrote none, so the first two were reconstructed at landing from the committed artifacts and the commit…
Opened 2026-10-21. Hunt #137. This is the second track of the campaign the owner directed on 2026-10-21.
2026-10-21. Hunt #137, the numeric contour plan. Files: numeric_plan.py (the generator and the verifier), plan_T50.json, plan_T100.json (the plans), test_numeric_plan.py (pins and planted…
Written 2026-10-21 by the exact_argument role of the campaign workflow. Grades as in MISSION.md. Status: closed.
Written 2026-10-21 by the gamma_increment role of the campaign workflow. Grades as in MISSION.md. Status: closed.
Written 2026-10-21 by the horizontal_legs role of the campaign workflow. Grades as in MISSION.md. Status: closed.
Written 2026-10-21 by the low_height role of the campaign workflow. Grades as in MISSION.md. Status: closed.
Written 2026-10-21 by the statement-and-skeleton role of the campaign workflow. A plan, not a result . Grades as in MISSION.md: measured, hardened, kernel-checked.
Grade: kernel-checked by Lean's kernel (Lean v4.35.0-rc2, Mathlib 065356127b1dc0016f66b7283ce0ce2c4055aa55, zero sorry, axioms propext, Classical.choice, Quot.sound only).
positivity_geometry | unresolved | positivity_geometry/challenge/CHALLENGE_RIVAL.md probe_tower | restricted class obstructed | probe_tower/challenge/CHALLENGE_RIVAL.md ccm_arithmetic |…
Opened 2026-10-21. Hunt #150. The owner directed this hunt on 2026-10-21 as a genuine attempt at the Riemann hypothesis itself, beside the campaign's other tracks: build real constructions…
Synthesis, 2026-10-26. Written by the synthesis session, which built none of the six constructions and ran none of the challenges.
Hunt #150 , mechanism 1. Built 2026-10-21, written up 2026-10-26 when the owner resumed the hunt in place. Status: constructed and measured; not challenged yet; unreviewed by any person.
The 2026-10-21 runs were single-process Python on the campaign box , at most four processes of the session alive at once.
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. rival_gate.py independently assembles the even-sector Galerkin matrices from the displayed formulas, using…
Hunt #150, mechanism 1. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Hunt #150 , mechanism 2. Built 2026-10-26. Status: constructed, measured and pushed to a located obstruction; not challenged yet; unreviewed by any person.
Single-process Python on the campaign box , commands from the repository root with .venv/bin/python, at nice 10, at most four processes of this session alive at once.
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. rival_gate.py imports no mechanism or other-hunt module.
Hunt #150, mechanism 2. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Hunt #150 , mechanism 3. Built 2026-10-21, written up and its prime-side run made on 2026-10-26 when the owner resumed the hunt in place.
Single-process Python on the campaign box , commands run from the repository root with .venv/bin/python.
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. rival_gate.py imports none of the mechanism modules.
Hunt #150, mechanism 3. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Hunt #150 , mechanism 4, built in the session of 2026-10-21.
Kept in this directory rather than in a hunt-level file, because six sessions share one worktree and a shared file invites lost writes.
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. The independent calculation is rival_gate.py; it imports no file from the mechanism.
Hunt #150, mechanism 4. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Hunt #150 , mechanism 6. 2026-10-21. Status: constructed and pushed to a located obstruction; not challenged yet; unreviewed by any person.
All runs were single-process Python on the campaign box, started at nice 10, with at most two processes of this session alive at once and the 1-minute load average between 37 and 65 while…
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. The exact template and rival calculations in rival_gate.py are an independent implementation and import no mechanism…
Hunt #150, mechanism 6. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Hunt #150 , mechanism 5. Built 2026-10-26. Status: constructed, measured and pushed to a located obstruction; not challenged yet; unreviewed by any person.
Single-process Python on the campaign box , commands from the repository root with .venv/bin/python, at nice 10, at most four processes of this session alive at once (two of them are this…
Role: rival-gate challenger, 2026-10-26. I did not build this mechanism. rival_gate.py imports no mechanism or other-hunt module.
Hunt #150, mechanism 5. Circularity challenger, 2026-10-26, branch hunt/rh-moonshot-challenge-circularity. This session did not build the construction and edited none of its files.
Formerly THEOREM.md. Renamed on 2026-10-10 because the claim that name announced was withdrawn by the audit below; the file now records the audit and, under a separate heading, the…
Grade: ordinary argument, unreviewed, recording a known result. The equivalence is classical, not new and not this hunt's: main states it in hunts/epp_herglotz/RESULTS.md (its verdict…
Question: does every nontrivial zero of zeta have real part 1/2. Both proof and disproof count as success. No assumption of RH, no equivalent, no stronger unproved claim, no extra axioms.
Grade: measured , throughout. No violation found, no support claimed. Every Li row in this file is graded measured, including the Arb-ball rows of phases 2 to 4 .
Run records from 2026-10-03. The enclosure grades the outcome lines originally stated were withdrawn by the audit of 2026-10-04 ; on 2026-10-10 those lines were regraded to measured…
What was wrong: enclose_li_mid.py bounded the midpoint-rule remainder with M2c = 2M/^2, the Cauchy bound for f'' where f = log xi.
Target: decide whether every nontrivial zero of the Riemann zeta function has real part 1/2. Proof and disproof have equal standing.
RH is unresolved. No proof or disproof is claimed. This checkpoint gives ordinary proofs of two scoped intermediate statements, exact algebra checks, and bounded floating-point comparisons.
Fresh isolated worktree, starting at origin/main 8feec794. Shared checkout and its uncommitted files were left untouched.
Base: origin/main a9f0b38b, isolated worktree. Baseline: 64 passed, 5 slow tests deselected, 3 existing expected failures in 7.37 seconds.
RH remains unresolved. Two concrete square constructions were developed and both fail for the actual theta kernel.
Target: the Riemann Hypothesis, through Robin's criterion (RH iff sigma < e^gamma n log log n for every n > 5040).
Status: candidate, ordinary derivation, unreviewed, pending external verification. The numerical step is enclosure-carrying (Arb balls, cross-checked by a second quadrature route); the…
Estimate before spending: the whole computation is a few hundred Arb operations (under 1 s); the test file sieves to 3 10^6 and sums logarithms at 30-40 digits (about 35 s on the M4).
Assembled 2026-08-17 by eleven parallel literature surveys; each entry carries the URL its statement was checked against, or is marked memory-unverified.
Scores are the surveying arm's (importance, novelty probability, tractability, verifiability, computational leverage, each /10; sat = literature saturation, high is bad).
This hunt was worked on claude/riemann-hypothesis-research-ofds8s between 2026-08-17 and 2026-08-18 and never landed. Hunt R-F00E48 landed part of it.
Opened 2026-08-17 on branch claude/riemann-hypothesis-research-ofds8s.
All commands run from the repo root with the project venv . The Arb backend must be live: .venv/bin/python -c "from zeta import rigor; print" should print python-flint.
Sub-study of hunts/rogue_frontier/. Opened 2026-08-18.
Running log. Appended as things happen, because a session can be killed at any moment and a result held only in a chat window is a result that is lost.
Opened 2026-08-18. A scope extension of rogue_frontier, recorded here rather than assumed: the campaign's HuntSpec question is about the RH-adjacent frontier, and this sub-study is not…
Sub-study of hunt #38 (hunts/rogue_frontier/MISSION.md carries the governing HuntSpec). Opened 2026-08-17.
Session of 2026-08-17. Grade: measured, with enclosure-checked arithmetic (every headline d_N^2 is an arb ball that rigorously contains the exact value of the stated finite-dimensional…
Every formula this study implements was read in at least one primary source during the session of 2026-08-17; the two load-bearing statements (Vasyunin's formula, the BCF asymptotic) were…
Status: ACTIVE. Opened 2026-08-17. Nothing here is a result until it survives the campaign's destruction stages; grades follow the repository ladder.
Status: probe output of the sine_gram hunt. Everything below is a statement about the CUE band-Gram model at band ratio lambda = d/N (equivalently, in the limit, the sine process of unit…
Constructive derivation of the Guinand-Weil explicit formula for the Davenport-Heilbronn function in repository normalization, with the exact statement of what is argued, the finite-pairing…
A sub-study of hunts/rogue_frontier/ (its MISSION.md and HuntSpec govern here). Opened 2026-08-17.
Study of 2026-08-17, hunts/rogue_frontier/weil_trunc/. Sources, exact construction and claim inventory: SOURCE.md.
Step-0 verification record, written before any implementation. All PDFs were fetched 2026-08-17 and read; page/equation citations below are from those copies (stored in the session…
Feasibility evaluation and quantitative dictionary gate for the Davenport-Heilbronn (c=31, N=60) cell toward an off-line-zero detection result.
Goal: first (c, N) where the DH truncated Weil form acquires a negative eigenvalue, enclosure-checked, with zeta control and localization evidence.
Exploratory study under hunts/rogue_frontier/. Per hunts/README.md, nothing here is a promoted result; every number below carries its rung on the repo's certainty ladder, stated inline and…
Session scratch log, updated incrementally. Nothing here is a result until it reaches RESULTS.md section 9 with a grade.
Opened 2026-10-21. Hunt #145. This is the rung3-pilot lane of the campaign the owner directed on 2026-10-21 (route 3, "Rung 3: kernel-checked Davenport-Heilbronn zero").
Hunt #145, 2026-10-21. To the owner, from the rung3-pilot lane. This memo asks for a decision; it launches nothing.
Hunt #145, lane rung3-pilot, 2026-10-21. Grade: measured (one box, one session, one route per number) for every cost below.
Hunt #145, searched 2026-10-26 with web search (four queries, one of them in the thorough mode). The question: has anyone kernel-checked, formally verified, or rigorously enclosed an…
Hunt #145, written 2026-10-26, revised the same day after the whole-tower re-pilot. The owner granted the production window on cloud compute that day (MISSION.md, "Owner decision…
Hunt #145, closed 2026-10-26. Grade: kernel-checked (Lean 4 v4.35.0-rc2, Mathlib 065356127b1d, zero sorry, only propext, Classical.choice and Quot.sound), pending external verification.
The swarm box <box>: 32 vCPU reported as "Intel Core Processor (Haswell, no TSX)", one thread per core, 115 GiB, no swap, shared with other workflows. Times are UTC.
RESULTS.md and RUNS.md cite these as <cache>/rung3-ball-production-full/... and <cache>/rung3-conron-fleet-20261027. They were on one machine only.
Opened 2026-10-16 as Hunt #134; Hunt #139 on main (renumbered at landing on 2026-10-21, because #134 on main is gauss_positivity and #136 to #138 are taken).
Hunt #139 (opened as #134), 2026-10-16. Status: answered within its stated scope; unreviewed by any person.
Every run, including the ones that produced nothing. All on a cloud container; nothing ran on the operator's machines.
Recorded 2026-09-12. A second delegated session, given the gating audit and told to break it, working independently against the same commit of anthropics/formal-math and Wang…
Recorded 2026-09-12. This is the gating audit for MISSION.md §6, run read-only against anthropics/formal-math at commit fbdc36bbf17d20af3fd0447c6d1a8a02773c9844 and against Wang…
Landing note, 2026-10-30; name restored 2026-11-01. At landing the correspondent's name and account handle were withheld, because this record quotes private contact-form messages and the…
Opened 2026-09-12. Nothing in this directory is a result. Nothing here bears on RH .
Written 2026-09-12 against anthropics/formal-math at commit fbdc36bbf17d20af3fd0447c6d1a8a02773c9844 (every file:line below is relative to zeta23/), Wang arXiv:2609.07918v1 (Sections 1 to…
The hunt was opened on 2026-09-12. Sections 1 to 3 are three findings from that day, all reading and measurement rather than new mathematics, which between them killed the plan the hunt was…
Estimates before launch, outcomes after, including runs that produced nothing. Per CLAUDE.md: nothing heavy on the operator's machines, GitHub Actions is the default compute, and anything…
Opened 2026-10-26. Hunt #152. Part of the compute sweep the owner funded on 2026-10-26: walls the record calls cost walls rather than mathematical ceilings, to be knocked down with hardened…
Committed on 2026-10-26 in its own commit, before any rerun result exists. The failed gate at omega = 727.95134 (RESULTS.md section 6) stays recorded as it is, whatever this rerun finds.
Status on 2026-10-27, three outcomes and one post-hoc finding:
Every estimate is written here before the spend. Box: shared 32 vCPU Linux VM, python-flint 0.9.0 , nice -n 10, with a co-tenant holding the 1-minute load near 30 to 65 during these runs…
A support run launched from fulcrum for the run behind hunts/r_186989/.
Hunt, not a result. Nothing here is evidence for or against RH .
Bounded question, set by the parent run 0897a5a7 / Hunt #91 : reconstruct the Erdős–Turán 1934 proof in modern notation, isolate every place the factor 2 per prime is lost, and test whether…
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Support run 5418c63e, 2026-08-24, for run 872d7dce . Instrument: probe_arm_b.py (runs end to end in ~7 s; --quick in <1 s). Data: results.json. Nothing here bears on RH .
Support run for 0897a5a7, answering one bounded question for a live parent: improve the hunts/r_186989 computation so that it ranges over choices of $S$ instead of freezing the first $k$…
Hunt, not a result. Nothing here is evidence for or against RH .
Support run for hunts/r_186989 (Erdős #126). Arm label construction-refutation: search for algebraic, CRT, recursive, tensor or composition constructions giving $|A|$ exponential in $|S|$…
Hunt, not a result. Nothing here is evidence for or against RH . Support run for r_186989, arm label construction-refutation.
This is a hunt. Nothing here is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
Support run 78c499b4-bc7d-4e1a-9efa-47571547b826, 2026-08-24. Serving run 872d7dce (hunt r_c7f779), which asked one bounded literature question and is still alive to receive the answer.
Support run 78c499b4, 2026-08-24, for run 872d7dce . This is the prior-art page the brief called arm_e/PRIOR-ART.md.
Support run for 0897a5a7 / hunts/r_186989. One bounded question:
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing here is a result, and nothing here bears on RH .
Hunt, not a result. Nothing here is evidence for or against RH .
A bounded support run for run 0897a5a7, launched from fulcrum.
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
Bounded question. Study $M{ij} = a_i + a_j$ (rank $\le 2$, off-diagonal entries $S$-units). Find and apply the literature on low-rank matrices over finitely generated multiplicative groups.
Hunt, not a result. Nothing here is evidence for or against RH .
Support arm for run 0897a5a7. Bounded question, one lane:
Hunt, not a result. Nothing here is evidence for or against RH .
A hunt, not a department and not a result. Nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH .
What this is. A support run launched by run 0897a5a7 to answer one bounded question: is there a genuinely joint multi-prime pruning argument for Erdős Problem #126?
Hunt, not a result. Nothing here is evidence for or against RH .
This is a hunt. Nothing in hunts/ is a result, and nothing here is evidence for or against RH .
Hunt, not a result. Nothing here is evidence for or against RH . Support run for 0897a5a7. Arm label: sunit-equations.
A support run, not an open hunt. Another run asked one bounded question and is waiting on the answer, so this directory records the answer and the evidence behind it, and then it is closed.
The answer: yes. At dps=60,
What this is. An adversarial audit of hunts/r_186989/RESULTS.md (Erdős Problem #126, Hunt #91). Every claim in that file was treated as hostile input: re-proved, re-computed independently…
Hunt, not a result. Nothing here is evidence for or against RH .
Support run for 0897a5a7. Bounded question: ignore the three lanes of the earlier brief, design a proof program for Erdős #126 (log g = o from the statement and the original theorem, rank…
Hunt, not a result. Nothing here is evidence for or against RH .
A support run launched by run 0897a5a7 (the Erdős #126 scout, r_186989) and routed through fulcrum. One arm, one bounded question.
Support run for 0897a5a7 / r_186989. A literature map, not a new theorem. Nothing here is evidence for or against RH .
Status: design only, nothing implemented, no compute run. Owner: Scholar, 2026-10-29. Scope: turn the hardened negative cell of weil_propagation/numerics/RESULTS.md §3.2 (N = 256, c ≥…
Opened 2026-10-21. Hunt #146. Branch hunt/weil-dh-line, worktree .claude/worktrees/weil-dh-line, from origin/main at fb647bfc7.
Hunt #146 , opened 2026-10-21, items 3 to 6 completed or priced on 2026-10-26 after the owner resumed the lane. Question, windows and rules: MISSION.md.
Date 2026-10-29, revised 2026-10-30 at landing. Work for DESIGN-kernel-negative-cell.md. No claim about the continuum form is made or changed here; this is about one finite band matrix.
Box: the swarm box (32 vCPU, 115 GiB, no swap), shared with other workflows. Python is the repository .venv (python-flint 0.9.0 with the Arb backend, numpy, scipy with HiGHS).
Scope: hunts/weil_gram/ only. Nothing outside this directory is modified. Status: exploratory. Nothing here is a result about the Riemann Hypothesis.
Nothing here is a result about the Riemann Hypothesis. This measures the bottom of the Weil form on Gaussian subspaces. Grade: measured.
Opened 2026-09-23 on branch teal-sea/weil-propagation, which merges teal-sea/rh-strategy-council-sep17 (the Davenport-Heilbronn negativity result at (c, N) = (31, 60)) onto origin/main.
Opened 2026-09-23 on branch teal-sea/weil-c4-s2, based on teal-sea/weil-propagation-theory at f723209. Approved by the operator on 2026-09-23.
Coordinator's summary, 2026-09-23/24, branch teal-sea/weil-c4-s2, nothing pushed; lines 1, 2, 4 and 5 updated on 2026-09-24 after the Modal follow-up and the rho follow-up (MISSION.md, last…
You own hunts/weil_propagation/c4_s2/assembler/ and hunts/weil_propagation/c4_s2/delta_t_bound/ (create it), and write nowhere else.
Written 2026-09-24 on branch teal-sea/weil-c4-s2 by the assembler/ worker, under assembler/BRIEF.md . Committed before any ε exists.
You own hunts/weil_propagation/c4_s2/bound_quad/ and write nowhere else (except appending to c4_s2/modal/RUNS.md if you use Modal). Time box: 3 hours from your start.
Started 2026-09-24 17:35 -0500, time box 3 hours . Section 1 is the plan (milestone 1), committed before any bound was coded. Section 2 is the derivation (milestone 2).
What this folder delivers to assembler/ and referee/ (BRIEF.md, "The bound interface"). Derivation: DERIVATION.md s2. Outcome: RESULTS.md.
Folder of the error-bound follow-up of 2026-09-24 (BRIEF.md, MISSION.md last section). Started 17:35 -0500; plan committed at ab0f8fa (DERIVATION s1), derivation, code and tests at 747487f.
You own hunts/weil_propagation/c4_s2/bound_trunc/ and write nowhere else (except appending to c4_s2/modal/RUNS.md if you use Modal). Time box: 3 hours from your start.
Worker bound_trunc/, 2026-09-24, branch teal-sea/weil-c4-s2, from 17:35. Every argument here is an ordinary argument by this worker, unreviewed until referee/ has read it.
For assembler/ and referee/. Import with sys.path.insert(0, "hunts/weil_propagation/c4_s2/bound_trunc"), then import eps_trunc. Python: PYTHONPATH=<worktree root> .venv/bin/python.
Worker bound_trunc/, 2026-09-24, 17:35 to about 18:40 (box to 20:35), branch teal-sea/weil-c4-s2. Brief: BRIEF.md .
You own hunts/weil_propagation/c4_s2/checker/ and write nowhere else.
Phase 1 (independent of kernel/ and two_adic/, which were not read).
1. T_S reached the checker, and R_S = Q - T_S is measured on all nine cells, now under two_adic/'s QR rho (c3dca00; all eleven units rebuilt on Modal, s7.8).
You own hunts/weil_propagation/c4_s2/cutoff/ and write nowhere else. Time box: 2 hours of work from your start.
Gap : product-ball cutoff against the module cutoff, S = {∞, 2}. This folder builds no trace term. It holds the checks behind RESULTS.md.
Worker cutoff/, 2026-09-23, branch teal-sea/weil-c4-s2. Nothing here is a claim about RH. The conclusion on c ∈ 2, 3) is known (Zhu arXiv:2608.24827); this folder only asks which cutoff the…
Worker assembler/, 2026-09-24, branch teal-sea/weil-c4-s2, under assembler/BRIEF.md and assembler/PREREG.md. Grades follow the AGENTS.md ladder, weakest step governs.
Written 2026-10-26 for PREREG s1 (with amendment 1). Code: bounds.py; tests: test_bounds.py. Grade of everything in this file: derived (ordinary arguments), unreviewed, resting on the two…
Bounded attempt (allowance: five agent-days) at the bound the brief asks for: ‖ΔT_exact − ΔT^‖₂ as a function of the mode count n, below 1.18e−2 at n = 280 on c = 2.9, or a recorded…
Opened 2026-10-26 on branch hunt/c4-exact-gram (off origin/main at 558eee037) as a resumption of the C4 line in hunts/weil_propagation/c4_s2/, under the owner's compute sweep of 2026-10-26…
Written 2026-10-26 on branch hunt/c4-exact-gram. Committed before any rebuilt row exists: at this commit no rebuild module exists, no block has been computed, and the only computation run…
Folder of the compute sweep's C4 resumption . Pinned by test_exact_gram.py: the block timings and estimates (price_block.json, estimate.json), E1 at the registered and stored S, the…
Every estimate here was written before the spend it prices. Box: the shared 32 vCPU / 115 GiB Linux VM, python-flint 0.9.0 (Arb backend confirmed, zeta.rigor.BACKEND = python-flint)…
You own hunts/weil_propagation/c4_s2/kernel/ and write nowhere else. Time box: 3 hours of work from your start. At the box, write RESULTS.md with what stands and stop.
For two_adic/ and checker/. Import from the worktree root with sys.path.insert(0, "hunts/weil_propagation/c4_s2/kernel"), then import sonin. Python: PYTHONPATH=$PWD .venv/bin/python.
Worker session of 2026-09-23 on branch teal-sea/weil-c4-s2, folder hunts/weil_propagation/c4_s2/kernel/. Nothing here is a claim about RH. Grades follow the AGENTS.md ladder.
You are the compute worker. This folder runs the two compute proposals the mission left open (c4_s2/RESULTS.md line 4 and on Modal.
1. What ran: all eleven checker/ units, all with status ok, on Modal, from a clean clone of the tree at e2b46a5 whose T_S input digest is b2e7787bce7a, the same as the local call.
Every run of run_modal.py on Modal, with the estimate written before the spend it covers (AGENTS.md compute discipline, rule 3). Hard cap: 25 USD.
You own hunts/weil_propagation/c4_s2/referee/ and write nowhere else. Time box: 3 hours of work, not counting time waiting for routed material.
Verdict. The two derivations that carry the follow-up's outcome survive review: bound_trunc/'s Lemma 1 (both truncation tails are infinite traces) and Lemma 3 with its Corollary 3.1 (the…
You own hunts/weil_propagation/c4_s2/two_adic/ and write nowhere else. Time box: 3 hours of work from your start. At the box, write RESULTS.md with what stands and stop.
Shared basis and cells as in ../MISSION.md: U_n = L^{-1/2} exp on 0, L, L = log c, n = −N … N, index 0 = n = −N; a quadratic form F is the matrix M with F = v M v for f = Σ v_n U_n; inner…
Worker two_adic/, 2026-09-23, branch teal-sea/weil-c4-s2, time box 21:10 to 00:10, closed at about 22:45 with T_S evaluated. Nothing here is a claim about RH.
Written 2026-10-21 on branch hunt/weil-ghost-zeros (from origin/main fb647bfc7), lane "ghost-zeros" of the existing hunt weil_propagation.
1. P is confirmed, with a wide margin (hardened, band N = 128). At each of the seven preregistered windows, c = 29, 30, 61/2, 245/8 before the N = 128 even crossing c128 in (30.646484375…
Machine: the shared swarm box (32 vCPU, 115 GiB), 1-minute load average 58 to 216 during these runs (other workflows), MemAvailable above 77 GiB throughout.
Read first: hunts/weil_propagation/MISSION.md, AGENTS.md (hard rules, certainty ladder, compute discipline), then hunts/rogue_frontier/weil_trunc/RESULTS.md sections 2, 4, 8 and…
2026-09-23
Worker: numerics, branch teal-sea/weil-propagation, 2026-09-23. Scope and kill-control: ../MISSION.md, brief: BRIEF.md. Nothing here is a claim about RH.
Machine: an M-series laptop, 16 GB. Every run is single-process, under 10 minutes, under 1 GB, checkpointed per unit .
Read first: hunts/weil_propagation/MISSION.md, AGENTS.md (certainty ladder, original vs novel), ALIGNMENT.md, then hunts/rogue_frontier/weil_trunc/RESULTS.md and THEOREM_FEASIBILITY.md (the…
Read in full or in the relevant sections (local copies in the session scratchpad, not committed):
1. Strongest candidate was C2 (Levy-Markov + pole); as a positivity/propagation mechanism it is now refuted (line 3), and no candidate survives.
Scope: hunts/weil_split/. Nothing outside this directory is modified. Status: exploratory. Nothing here is a result about the Riemann Hypothesis.
Independent recomputation from the specification, 2026-10-30. Nothing here is a result about the Riemann Hypothesis. This note only checks one identity for one family of test functions.
Nothing here is a result about the Riemann Hypothesis. This is an exact place-by-place decomposition of the prime side for one family of compactly supported test functions.
Written for an agent starting cold. Read MISSION.md for scope, RESULTS-xiprime.md for the finished piece, RESULTS-higher-derivatives.md for the blocked one. This file is the operating state.
A breadth-first search for one externally checkable mathematical contribution adjacent to the Riemann zeta function, run under the laboratory's standing controls.
Status: a measured obstruction and a located piece of buried prior art. Not a result about zeta. Nothing here is evidence for or against RH.
Status: one exact collapse result, a full reproduction of every number the public artifact makes reproducible, and one measured gap between the paper's prose ceiling and the finite law…
Status: exact-rational evidence package for independent review. This file strengthens the ambient variational result in RESULTS-xiprime-global-optimality.md.
Snapshot: 8b10ede734258e9e966f6b889176d81a4d59964d Verdict: Outcome A. The full Hilbert-space window optimization is a coercive quadratic minimization, and its unique optimizing ray has a…
Status: measured, and independently reproduced three ways. Not a new analytic theorem, an optimisation, run to its exact answer, of a functional somebody else derived.
Hunt #75 closed the note-to-colour question and, in its aftermath, the operator asked for something bolder.
The reading path, derived line by line. Laid out in order on the reading page; listed here for completeness.
Zeta Lab is a computational and formal workbench for studying the Riemann zeta function, attempting original mathematics toward the Riemann Hypothesis , and establishing useful intermediate…
Or: "is the harmonic series / Riemann-sum thing actually connected to the zeta function and to derivatives?", yes, and here is exactly how.
"Can you model the theta function with a differential equation?"
Riemann's functional equation is not a coincidence you verify afterwards; it is a change of variable.
"What do the zeros actually have to do with the primes?"
The payoff of docs/02-theta-heat-and-modularity.md. There we watched heat flow produce Xi. Here we run heat flow on Xi and ask how the zeros move.
Or: the spectral dream. Why "there ought to be a differential equation behind this" is the right instinct, why nobody has produced the equation, and why the zeros nevertheless behave…
A curated catalogue of statements exactly equivalent to RH, with honest notes on which ones have ever gone anywhere.
The mathematical tools in this repository have proved many useful statements. Their current estimates do not by themselves establish RH.
The sequel to docs/08-why-it-is-hard.md. That document catalogued why the existing tools provably stall.
"The explicit formula looks like modal analysis. So what is the structure, and who gets to tap it?"
A companion to docs/09-new-ontologies.md. That document surveyed the "new objects" landscape and docs/10-trace-formulas-and-connes.md slowed down on the trace-formula corner; this one slows…
docs/08-why-it-is-hard.md catalogued what fails. docs/09-new-ontologies.md described the one time a rebuild worked.
The moments programme starts with a data contract, not a formula. The lab's local cache reaches only the low thousands in height; the external tables that matter live at much larger indices…
A companion to docs/12-how-hard-problems-die.md. That document is a kill board: eight problems, the mechanism that killed each, and RH scored against them.
Building the Polya-Hilbert Operator Computationally
The goal of the current sprint is to pass the Counting Gate. To do this, we must build a computational model of the Poisson-summation map on the Adelic Schwartz space, and demonstrate that…
A methods retrospective. Everything in docs/00–16 is about the mathematics; this document is about the refereeing.
A session's worth of deliberately improbable attacks on RH, each pushed until it either produced something measurable or hit a named obstruction. None of them advance RH.
A side project, and a probe rather than a department, see §6, which is the most useful part of this document because it is the part that says no.
The architectural record of the 2026-08-09 build: what was latent, how it was attacked before it was built, what survived, and where it stops.
Status when this file was committed: pre-registration only. No result in it. Everything below §5 was written before the gate existed, before any case was run, and before any number was…
Abstract The Riemann Hypothesis possesses numerous mathematically equivalent statements (Li's Criterion, Weil Positivity, Mertens' Conjecture, etc.).
Status of this file when it was committed: pre-registration only. Nothing in §§5–8 existed. No number below §4 had been measured.
An ontology attempt in the sense of docs/09 §4: propose a structure, push it at the gates, and record exactly where it bleeds.
2026-08-10/11. An operator handed the laboratory over with no theorem, no direction, and no assurance that the agenda was the right agenda.
ROADMAP.md ("The outside memos, triaged") records the decision; this document records what landed the same day, what each piece can and cannot claim, and where each one's honest edge is.
12 August 2026. A reading of the laboratory's current frontier work, written because the state changed four times in one day and the front page carries only the conclusions.
Disposition of the cheapest informative slice of meta/asymmetry-experiment.md. Run 2026-08-20, four checkers. Grade: measured, one run each.
Hunt #61 produced, so far as the literature search recorded in hunts/lambda_dh_bounds/NOVELTY.md reaches, the first quantitative bounds, from either side, on the de Bruijn-Newman constant…
A reading-course page about a threshold this laboratory did not discover. The threshold that governs the rightmost zeros of the prime zeta function is not this laboratory's result: it is…
Hunt #65 adjudicated two contradicting kappa = 2 tables in this repository and, in doing so, located the error that produced the disagreement. It is not in either table's code.
21 August 2026. On 18 August 2026 the Lean FRO and ICARM opened Palomar, a registry of Lean-verified mathematics, described by its own documentation as the analogue of a preprint server for…
Hunt #75 . Verdict: PRETTY BUT TRIVIAL for the note-to-hue question; the reformulation in section 9 is the one worth keeping.
Hunt #76 . Verdict: INTERESTING STRUCTURE, classical in substance. Measured in steps-per-octave, the Riemann zeros avoid the equal temperaments that tune prime-power harmonics and ignore…
Hunt #110, hunts/outband_intake/. Read hunts/outband_intake/RESULTS.md for the measurements and the doors.
Moved off the front page on 2026-09-05. README.md is an index, and AGENTS.md says so in as many words: "Keep README.md an index, not a manual.
This is the cross-hunt index of method. hunts/README.md logs each hunt by outcome; nothing there says which trick a later hunt could pick up. This file does.
7 October 2026. On 2026-10-06 OpenAI published github.com/openai/math (Apache-2.0, one commit, adc7f1241b42e322a6451854ab7e4b4c146bf78a): 722 manuscripts in 372 result families produced by…
Every result below except the first is conditional on OpenAI's theorem. Four of them (hunts #123 to #126) are proved, given OpenAI's theorem: the argument is an ordinary written proof by…
Hunt #127, hunts/euler_defect_axis/. The measurements and the doors are in hunts/euler_defect_axis/RESULTS.md; the audit that rewrote it is in AUDIT.md; the repair it proposes to files a…
Hunt #129, hunts/epstein_height/. Measurements, the guard and the doors in hunts/epstein_height/RESULTS.md; the audit that rewrote this page's title in AUDIT.md.
Hunt #130, hunts/quotient_exponent/. Measurements and doors in hunts/quotient_exponent/RESULTS.md; the audit that rewrote this page's conclusion in AUDIT.md.
Hunt #131, hunts/claim_halflife/. The measurements, the controls and the doors are in hunts/claim_halflife/RESULTS.md. This page is the front door.
Hunt #135, hunts/jensen_wedge/. The derivations, the reviews and the doors are in that directory; RESULTS.md sections 18 to 20 carry the landing. This page is the front door.
The theorems are finite. The height-100 result says nothing above 100 or about the Riemann hypothesis .
Upstream artifact. DH_census_v6_package.zip, SHA-256 c50c0bcef907daa2fdfa30c92f6011edf4ef87eadd6467cf1b6e34eb0565355f, the single file of Zenodo record 23585903 (published 2026-10-23, title…
Riemann's zeta function satisfies a functional equation, xi = xi(1 - s), and all of its zeros that anyone has computed lie on the line Re s = 1/2.
Hunts #155, #156 and #157. The records are hunts/arch_cover/RESULTS.md, hunts/weil_gram/RESULTS.md and hunts/weil_split/RESULTS.md. This page is the front door.
Forty-nine numbered documents. The first five are a single argument and are meant to be read in order; everything after 14 is a record of a particular piece of work and can be read on its…
One page per way into the repository. A repository with several purposes does not get several repositories; it gets one verified core and several short entry points.
For you if you care less about the Riemann Hypothesis than about the problem it forced this repository to solve: when plausible ideas cost minutes to generate, the scarce resource is…
For you if you care about the difference between a number that is accurate and a statement that is proved, and want to work where nothing is measured.
LLVM IR rewrites, department #3, and the first whose subject shares no vocabulary with the mathematics: programs, not functions.
This door is for people who want to clone Zeta Lab, run their own agents against a bounded question and return the result as a pull request.
Subject. A frozen implementation of true union semantics for restricted day-of-month/day-of-week cron fields under the # (nth weekday) and W (nearest weekday) special forms, a feature added…
For you if you want to generate leads automatically, and, more usefully, to see what fraction of them survive.
For you if you want to see an LLM work against deterministic mathematical checks instead of an LLM judge.
Curves over F_p, department #2, and the first second subject: the same referee architecture under a property that is decidable.
For you if you want real intuition and real numerics about ζ, to watch the theorems occur rather than read that they hold.
Subject. Batteries themselves. The payload of every claim in this department is a harness.protocol.Department bundle, and the claims are about whether such a bundle deserves trust: not…
For you if you have a structural claim about the zeros, a spectral operator, a positivity argument, a pattern in the statistics, and you want to know whether it is about ζ at all before you…
Subject. The commonest claim in applied machine learning: "model B genuinely improves on the baseline." A subject here is a comparison, candidate pipeline, baseline, and the pair's own…
The Riemann zeta function and RH, department #1, and the worked example every later department should copy.
Zeta Lab should evolve from a zeta-specific research repository into a research operating system built around its validation harness.
Purpose: Identify the highest-value live research fronts in the current Zeta Lab repository and recommend how available parallel-agent capacity should be allocated.
Scan date: 2026-10-30. Nothing here is a result about the Riemann Hypothesis. The statements compared are the ones on origin/main in hunts/weil_split/RESULTS.md, hunts/arch_cover/RESULTS.md…
Documents written about the laboratory by parties outside a working session: strategy memos, portfolio recommendations, external evaluations, and the design for an experiment that has not…
Independent repo-side analysis, performed without seeing another model's prior evaluation. Grounded directly in git history and current file contents as of 2026-08-08.
Planning-only pass. Repository not modified. This document turns the prior recommendation (bounded internal probe: E1 intervention ledger, E2 Lab Rotation Benchmark, E3…
Contract = Rev. 2 + Rev. 2.1 patch. This document adds no rules; it sequences the work and specifies the one procedure the contract references but does not define: blind lesion authoring by…
Accepted. The asymmetry in Rev. 2 was inconsistent: success-shaped conclusions required both families, but KILL fired on either.
Planning only. Nothing implemented. This document supersedes the affected sections of e1-e3-experiment-protocol.md; everything not revised here stands as written there.
This packet is the only material the consultant receives before reveal. It contains no owner-authored lesion instance, diff, answer-key entry, surface wording, or benchmark output.
How an outsider gets into this tree, and the reports that attack its own results: the red-team pass and the null controls. The standing rules a worker reads first were on this shelf until they were cut from the site; they are still in the repository.
Zeta Lab accepts agent-assisted contributions. Clone the repository, let your tools investigate a bounded question, and open a pull request with the evidence.
Date: 2026-08-04 Code: zeta/surrogate.py, scripts/15_null_control.py, tests/test_surrogate.py Commits: 18967ff, 61e3cbf, bb634a8, e248d15 Answers: attacks A1–A3 of REDTEAM.md §3.
A computational and formal workbench around the Riemann zeta function.
Date: 2026-08-04 Scope: the moments build sequence 6814f9d..9bd6dd3 (module zeta/moments.py, scripts/14_moment_experiment.py, its tests, HANDOFF.md, ROADMAP.md, docs/13-moments.md).
How the pieces are built and why, plus the annotated reading list and the records the other pages cite.
Ostoyae boards for this repository's hunts. A board is an execution plan: which work items a run may attempt, their checks, and the append-only record of every attempt made against them.
Verdict: PROVISIONAL. The subject fits the protocol better than expected, all four roles have natural compiler-domain analogues, and both calibration directions work on the first attempt.
An experiment: can intent, definitions, provenance, evidence, failed attempts, proof obligations and verification status be represented so that an agent can perform and resume rigorous…
Expose a small, reproducible RL/evaluation environment from Hunt #80 without publishing private operating material.
A model gets read-only access to Frank Wikström's published Bloch certificate verifier. It must reproduce two archived certificate values, reproduce the published near-branch target, and…
At runtime this package downloads Frank Wikström's public Zenodo archive, bloch-computations-1.0.0.zip, record 10.5281/zenodo.21975862, and refuses to execute it unless its SHA-256 is…
Fetched 2026-08-11. Nothing here is part of the laboratory; these are other people's artifacts, kept local so instruments and literature checks can collide with them offline.
Everything under history/ is archival evidence of what the laboratory previously wrote, attempted, measured, or believed. It is not an instruction layer and it is not a current frontier map.
These files are byte-for-byte copies from zeta-lab commit 4cb2230b0ba9f2e73121d0794ae81e08da84d3f5, before the owner's 2026-09-12 clarification of the research mandate.
README.md says what the lab is. AGENTS.md says how to work in it. This file records the decisions: why the work went the way it did, what is deliberately not being attempted, what is known…
Every technique in this repository: Mellin transforms, the functional equation, contour integration, the explicit formula, is genuinely powerful, and every one of them has a known ceiling…
The short version. The Riemann zeta function starts life as the sum 1 + 1/2^s + 1/3^s + ..., which converges only when Re > 1, but extends uniquely to a function defined on the whole…
Standalone HTML pages that animate what the laboratory computes. They are illustrations, not results: nothing here is measured, tested for mathematical content, or cited by any claim.
Written 2026-11-02 ~02:55 UTC. Branch mad/zero-visibility, worktree /home/thomas/zeta-lab/.claude/worktrees/mad-zero-visibility (on the Linux box), pushed to origin/mad/zero-visibility.
Branch mad/zero-visibility, worktree .claude/worktrees/mad-zero-visibility, from origin/main at b278389f3. Opened 2026-11-02 by an unsupervised session ("mad mathematician" brief).
Branch mad/zero-visibility (local only, never pushed), worktree .claude/worktrees/mad-zero-visibility, base origin/main at b278389f3. Session of 2026-11-02. Scope and rules: lab/MISSION.md.
The proof-agent adapter's durable ledger (lean/proof_adapter.py; contract in docs/26 §4). Every submission is recorded here with its project id so any later session can collect.
Surveyed 2026-08-31 against the Mathlib checked out at lean/.lake/packages/mathlib, pin v4.33.0-rc2 (lean/lake-manifest.json, toolchain leanprover/lean4:v4.33.0-rc2).
Problem. For r >= 3, must every r-colouring of the edges of K{r^2+1} contain r+1 vertices whose induced K{r+1} is missing a colour? Proved for r = 3, 4 (Erdős–Gyárfás 1999).
Target: hardyZ Status: Ready to draft Lean code Workspace: lean/ZetaLean/ Target Host: leanprover-community/mathlib4
Palomar is a registry of Lean-verified mathematics, incubated by the Lean FRO and ICARM and opened for submissions on 2026-08-18.
To set up your new GitHub repository, follow these steps:
Lean 4 declarations this laboratory formalized because it needed them, kept here rather than sent upstream.
Toolchain leanprover/lean4:v4.33.0-rc2, Mathlib v4.33.0-rc2 .
audit-v2-frozen.log in this directory is the #print axioms output for the Palomar V2 surface, committed so that the claim does not rest on a log that expires.
Ainta's simple-zero argument, assembled in Lean 4 as a theorem about Mathlib's riemannZeta and generalized to n points.
Plan file: rung3_plan2.json. The naive boxed-s lower-bound evaluation is gone; the small-square frontier is now certified by point enclosures on a grid + a Lipschitz bound L, where L = M/…
Formalize the least character nonresidue bound from hunt 125, Theorem 1, against OpenAI's exact Dirichlet L-function theorem.
Status, 2026-10-10 UTC: the initial package, OpenAI bridge and all eight axiom reports passed on Modal at source a4d02931.
The corrected run at source a4d02931d45ab42960cb6df9cbc7f608dc25cebd passed: https://modal.com/apps/teal-sea/main/ap-sF08OfNwCIjUdIWgfEEpSf.
This file records the checks that were run on exactly the sources in this repository and how to reproduce them.
Source: https://github.com/anthropics/zeta-23-lean at 3635e74826a4c1fcece7d1cd2b6fa75e43a00510, the same revision previously consumed as a Git dependency.
Mathlib keeps docs/1000.yaml: the Wikipedia list of famous theorems, each entry tagged with the Lean declaration that proves it.
Phase 4, step 1: the schema and nothing else. No generators, no screens, no pattern hunting. This document defines what a candidate observation is, what can be concluded about one, what…
Generated by scripts/mathlib_gaps.py from docs/1000.yaml, snapshot 2026-08-06. Do not hand-edit; regenerate.
Companion to the course in docs/ (each doc cites what it leans on; this is the consolidated shelf). FREE marks items legitimately available online at no cost.