Independent exact certification of machine-generated mathematics — exact arithmetic, no code shared with the claimant, refusal as a verdict. You can disagree with a result on this site by running something, and the disagreement is then about the mathematics rather than about which of us is more credible.
the job
Narrow, and not solving
Take a numerical claim someone already believes — from a language model, from a published paper, or from my own draft — and either produce an interval that provably contains the true answer, together with the program that produced it, or report that the method did not reach one and stop there.
Much of the recent work is verification of machine-generated mathematics: AI-claimed results re-checked in independent arithmetic, each check first shown to fail on a deliberately broken copy of itself. The tools are interval arithmetic with outward rounding, exact rational arithmetic — BigInt on one side, standard-library fractions on the other — Sturm chains, and contraction arguments of the Krawczyk kind.
I work alone, from Brazil.
three lines of work
What the reports decide
Audits of machine-generated mathematics (41). Claims produced by AI systems and autonomous discovery platforms — releases, registries, manuscripts, announced records — re-decided from their published bytes, by programs that share no code with the claimant. The series.
Evaluation whose ground truth is a proof (10). Graders measured against provably wrong answers, answer keys re-decided, and environments and benchmarks in which a certificate replaces the answer key. The series.
Theorems and exact values (28) and certified decisions for operations (10). Results proved here in exact rational or outward-rounded interval arithmetic — the calibration of the instruments, and some values that were not known. Engineering and operational numbers decided over declared envelopes: aviation, maritime, energy, ocean statistics. Each page names what it does not claim. Theorems · decisions.
the standard
Three things every page here owes you
The program, not a description of it. Every page is generated from the records it cites, and the repository — engine, instruments, certificates, corpus — is public under MIT with no dependencies. The detached verifiers run in the Python standard library: the next person to extend one needs neither my permission nor my machine.
Proof that the check can fail. A check that has never gone red is decorative — consistent with the code being right, and equally consistent with the check testing nothing. So every battery carries red controls, deliberate forgeries that must be caught, and every instrument is calibrated against a case with a known answer before it decides anything new.
The errors, dated, in public. Refuted claims are published with their generating mechanism named, and the machine’s own defects are recorded the same way. Every real bug this project has found was caught by a control, a calibration, an impossible number or a byte pin — or, since 2026-10-09, by an adversarial read of the code, counted apart; the erratum of that date is on the machine page. Since 2026-10-24, outside reruns have found defects too — three in one reading by maximusrufus, none moving a verdict (below).
what that does and does not buy
None of it makes the work correct. It makes it checkable, which is a weaker property and a more useful one.
outside the building
Where the work has gone, and what has come back
Credited elsewhere: what registries, claimants, columnists and curated lists have published about this work, each quoted from a snapshot pinned by sha256 (corpus/recognition.json).
Cited by a registry, 2026-10-18. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Three asterisks removed on our replays — C₃b, C₃c and C₇₁ — merged by T. Tao (pull request #216); the constants' pages cite the replays as [T2026]. In their words: “with no code shared with the claimants, by C. Toledo” (the source, pinned)
Cited by a registry, 2026-10-18. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): A fourth asterisk removed — C₃c's two-law certificate — on our replay, merged by T. Tao (pull request #230). In their words: “by C. Toledo, 17 Oct 2026; asterisk removed.” (the source, pinned)
Cited by a registry, 2026-10-18. The optimization-constants registry, constant 3b: The constant's page lists the replay as a reference of its own. In their words: “[T2026] Toledo, Carlos. Independent replay of the 13-point [MI2026] certificate” (the source, pinned)
Credited by the claimant, 2026-10-24. The Qiushi Engine authors (Oxelra-AI): The claimants credit the complete verification of all nineteen kissing configurations in their English and Chinese READMEs, linking the report and the programs. In their words: “Carlos Toledo has independently verified the complete configurations in all 19 dimensions, confirming their point counts and exact dimensions.” (the source, pinned)
Credited by the claimant, 2026-10-24. The Qiushi Engine authors (Oxelra-AI), Chinese README: The same credit in the Chinese README. In their words: “Carlos Toledo 已对 全部19个维数的完整构型完成独立验证” (the source, pinned)
Noted by an independent replayer, 2026-10-23. Maximusrufus, an independent replayer of AI-generated mathematics: Opening cert-machine issue 1, before re-running three of our records and finding no disagreement. In their words: “It covers much of the same ground, carefully, and I will cite it in our related-work notes.” (the source, pinned)
Written about in a column, 2026-10-29. Reg Saddler's column The Build (@zaibatsu on X): The column led with the replay of both labs' ETH proofs, and printed a correction: the outside check it had called missing had been done. In their words: “A Researcher in Brazil Replayed OpenAI's and Anthropic's Complexity Proofs” (the source, pinned)
Listed, 2026-10-26. Whataifound.org, a public tracker of what AI systems have found: Its entry on OpenAI's math release cites the kernel audit and the statement readings, and its no-outside-checks assessment was corrected on them. In their words: “Dated the initial no-outside-checks assessment and added MathVet and Carlos Toledo's cert-machine reports at their recorded OpenAI revisions” (the source, pinned)
Listed, 2026-10-17. Awesome-ai-proofs (a registry of AI-assisted mathematical results): Two of our audits recorded as audit events: the 4 × 4 matrix-multiplication decompositions (the row now marked verified) and the HorizonMath diagonal-Ramsey certificate (marked disputed). In their words: “Audit events from cert-machine (https://github.com/carlostoledo1891/cert-machine).” (the source, pinned)
Listed, 2026-10-06. Awesome-AI-Scientist (a curated list): cert-machine listed under peer review and verification. In their words: “cert-machine, Independent exact certification of machine-generated mathematics” (the source, pinned)
Listed, 2026-10-07. Plasma-ai/erdos, an open record of the Erdős problems: The δ₃ = 117/2192 result recorded as a claim on Problem 1186 (status: claimed), with the paper, the page and the archive. In their words: “title: Toledo's computer-assisted value of delta_3” (the source, pinned)
Listed, 2026-10-06. Erdosproblems.com, Problem 1186: Listed as a partial proof claim; the site says a listing is no guarantee of correctness and that nobody there has examined the proof. In their words: “claimed by Carlos Toledo (using Claude (Anthropic)).” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): C₈₄b corrected on our check: the row now records the note's theorem, 1.9993*, instead of its "suggested" 0.000719; merged by T. Tao (pull request #257), and the page cites the check as [T2026]. In their words: “[T2026] Toledo, Carlos. Interval-arithmetic check of the [Al26] chain” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Four more asterisks removed on our replay — the C₁a and C₁b step-function rows (Atris; EinsteinArena's AgentDiscover and CodexProLong) — merged by T. Tao (pull request #232) minutes after he stated the second-party rule; the two pages cite the replay as [T2026b]. In their words: “by C. Toledo, 18 Oct 2026; asterisks removed.” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Two more asterisks removed on our replay — C₁c and C₁d — merged by T. Tao (pull request #243), the C₁d bound now printed rounded up, above the value first printed; the two pages cite the replay as [T2026]. In their words: “by C. Toledo, 20 Oct 2026; asterisks removed, and the $C\_{1d}$ bound printed rounded up” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry, constants 1a and 1b: The constants' pages list the replay as a reference of their own. In their words: “[T2026b] Toledo, Carlos. Independent replay of the [A2026] and [EA2026] step functions for $C\_{1a}$ and $C\_{1b}$” (the source, pinned)
Cited by a registry, 2026-10-26. The optimization-constants registry, constants 1c and 1d: The constants' pages list the replay as a reference of their own. In their words: “[T2026] Toledo, Carlos. Independent replay of the step-function certificates for $C\_{1c}$ [R2026] and $C\_{1d}$ [CERT2026]” (the source, pinned)
Written about in a column, 2026-10-31. Giulio Prisco's newsletter Metafuturing week (@giulioprisco on X, an X article): The weekly column's item on the two ETH refutations cites the replay of both labs' Lean proofs on two kernels, and quotes the page's limit that a kernel cannot say what a statement means. In their words: “Carlos Toledo replayed both labs' Lean proofs on two independent kernels and found that both check against their own statements.” (the source, pinned)
Written about in a column, 2026-11-04. N365 ETH Watch, the Novelty ThreeSixtyFive newsletter on Substack: The explainer on whether the two ETH refutations reach the textbook ETH reads both labs' Lean statements, cites the replay on two kernels and the bridge proofs, and quotes the e-mail on what would move the verdict to certified. In their words: “We asked Carlos Toledo, who independently re-checked both labs’ proofs, to explain his result.” (the source, pinned)
Independently re-derived, no shared code — 30 September 2026. rainrzk (GitHub): λ(4) for Erdős #510 (reports/lambda4.html): the cubic, the 14 generic collisions and the nine families re-derived from the write-up with independent code; every finite case re-certified in interval arithmetic; every gcd-reduced 4-set with largest element ≤ 80 swept as a proof-independent control. Outcome: the same verdict; three documentation findings in the write-up, folded in (commit 1c248ca) (the audit · the thread).
Independently re-derived, no shared code — 23 October 2026. maximusrufus (GitHub): Twelve register rows re-decided with their own exact code, at cert-machine aa52e8d (Linux): the kissing configurations of AlphaEvolve (593) and EinsteinArena (594, 604); the sum–difference certificates of 3b (13 points) and 3c (147 and 95 points), agreeing to 30 digits; and six EinsteinArena constructions — two circles-in-a-rectangle (with the 44 overlapping pairs of the as-published Together AI packing), two Heilbronn convex, two min-distance ratios. A duplicated vector and moved probability weight are rejected by their check as by ours. Outcome: the same verdict on all twelve rows, no disagreement; two findings, both answered on the thread (the audit · the thread).
Re-run by a third party with the tools that wrote the record — 23 October 2026. maximusrufus (GitHub): The three ledgers re-derived with the tools that write them, at cert-machine aa52e8d (Linux, Python 3.14.4, Node v22.11.0); verify_sumdiff.py run beside the sum–difference ledger, its false-bound control firing. Outcome: every verdict and count identical (the audit · the thread).
Independently re-derived, no shared code — 24 October 2026. JeetuSK0808 (GitHub): The registry’s two C₃₁ rows (Lueker’s automaton at h = 9 and h = 10), our replay of reports/chvatal-sankoff.html re-derived with their own C program, written from Lueker’s published programs with no code of ours or the claimant’s: the state counts equal ours at h = 8, 9 and 10 (6,419,109; 51,425,006; 400,253,317); λ certified in round-to-nearest with an explicit inflation; γ₂ ≤ 0.8251007652 and ≤ 0.8241199563, below the printed bounds. Outcome: the same verdict on both rows; their bounds a little looser (vectors stopped once certified); their independence confirmed on the thread 2026-10-27 (the audit · the thread).
Independently re-derived, no shared code — 24 October 2026. JeetuSK0808 (GitHub): The registry’s C₈₄b correction (reports/optimization-constants.html §4) re-derived in their own interval arithmetic (mpmath), the note’s lemmas and inputs taken as given: c ≈ 0.000706 at the note’s choice; at most about 0.000707 over Y and X with R_K ≤ 103^d, and 0.00071385 with the regulator at its limit — so 0.000719 is not reached and 1.9993 is the entry. Outcome: the same verdict; their 0.00071385 is the maximum, our 0.0007150508 a ceiling above it (answered on the thread, where we printed 0.0007150507: the ceiling truncated, rounded outward since 2026-10-24) (the audit · the thread).
Re-run by a third party with the tools that wrote the record — 24 October 2026. maximusrufus (GitHub): The registry’s C₄₂ record (certs/turan-ledger.json) re-derived with the tool that writes it, at cert-machine 8924797: both rows identical. The rerun’s reading of instruments/turan/c42.py found three defects, none moving a verdict: failed checks answered REFUTED where the rule asks REFUSED, printed upper ends truncated rather than rounded outward, and the two routes compared on truncated strings. Outcome: the same verdicts (PARTIAL); the three defects fixed, recorded in the self-audit’s amendment of 2026-10-24 (the audit · the thread).
Independently re-derived, no shared code — 24 October 2026. maximusrufus (GitHub): Google’s AlphaEvolve Ramsey lower-bound graphs decided with their own clique search (two methods), before ours and with no code of ours: 15 of the 18 graphs, the verdicts compared with certs/ramsey-ledger.json. Outcome: the same verdict on all 15; R(10,12) and R(7,13), which they could not finish, decided here; R(8,18) unfinished on both sides (the audit · the thread).
Everything here is self-published and self-checked, so the honest question is what happens when it leaves. The record, with the status words meant exactly: first what has come back (20 of 112), then everything else, newest first.
Answered — sent 3 November 2026. The link for the organizers' ETH repository, as the 'announce your results' page asks: three lines to Mohan Paturi naming the page comment and https://carlostoledo.co/eth/. Sent by hand from Carlos's mailbox. (e-mail to rpaturi@ucsd.edu (a submission the organizers asked for on their page)). the text is step 2 of the 11-03 plan (this session); companion to ethdiscussion-announce-2026-11-03. REPLY 11-03 14:16/14:20 BRT (within 14 minutes), Ramamohan Paturi: "Thanks, Carlos" and "Thank you for the posting." — an acknowledgement, no question; nothing to answer.
Answered — sent 3 November 2026. The reply to a newsletter writer's e-mail (N365 ETH Watch, noveltythreesixtyfive.substack.com, received 11-03 in spam) asking what would move /eth/'s 'does not certify that ETH is false' to a certification and where the bridge between the two models stands: the plain quotable answer (the two model-equivalence steps are still prose, for the labs and for us), a contract-in-two-dialects analogy, the two third-party bridges' standing (both CERTIFIED as Lean theorems; TSavo's seam read DIFFERENT, not decided; Hawkley's predicate OpenAI's own), the quoting terms (verbatim with attribution and the link; the verdict words not paraphrased). Sent by hand from Carlos's mailbox. (e-mail reply to the newsletter's own address (answering a received e-mail; the channel rule)). outreach/n365-reply-2026-11-03.md; the Substack is nine days old with no ETH post at the time; the series was announced, not yet written. ANSWERED 11-03 ~23:30 BRT: the writer sent the full explainer before publication ('Did AI really break ETH? The small print between the proof and the textbook'), quoting the four passages verbatim with the verdict words as written and the Claude disclosure; checked here against the page and the e-mail — accurate. Carlos replied by hand (~01:00 UTC 11-04): permission to publish, two corrections (attribute the quotes to the e-mail, not the page; two kernels, three replays, not three kernels), one scope note (the lab's README sentence and the no-repeated-clause condition are theirs, unchecked here). When published: a recognition row from a pinned snapshot.; 2026-11-04 14:10 UTC: the explainer PUBLISHED (its link is on the recognition row), the three answers quoted verbatim and attributed to the e-mail, 'two kernels, three replays' as corrected; snapshot pinned and recognition row n365-eth-watch-explainer (kind press)
Merged — sent 23 October 2026. C₈₄b (the real sum–product exponent): the registry’s 1.999281 is the “suggested” c ≈ 0.000719 of Althoefer’s note, not its theorem c ≥ 0.0007; the chain decided in interval arithmetic holds at the note’s choice (c ≈ 0.000706) and gives c ≤ 0.0007150507 for every choice of its parameters; the row becomes 1.9993*, still asterisked (teorth/optimizationproblems pull request 257). drafted 2026-10-06 (outreach/github-p2a-2026-10-06.md item 7b) and held for a courtesy e-mail that the channel rule of 2026-10-23 dropped; the body now says Prof. Althoefer is welcome to supersede it; branch cut from 46dbf036, merges cleanly with #232, #242, #243 and #249 (and #235, #250, #251); evidence certs/sumproduct-ledger.json at 422b952 (re-derived identical 2026-10-23), the note’s tex pinned by sha256 and unchanged; 2026-10-23: a registry contributor who is not a maintainer (Chessing234) requested changes — the 28 May line kept 1.999281 beside the correction as if it were still the record, and the note should go at the top; the first point taken: the 28 May line corrected in place (24cf417, one 84b line), the second declined with the evidence (the section is not newest-first; #177’s own 10c correction went at the end); reply posted, description updated; 2026-10-24: JeetuSK0808 posted a separate check (mpmath): 0.000719 not reached, 1.9993 right; their 0.00071385 at the regulator limit vs our 0.0007150507 — ours a ceiling, theirs the maximum (we recomputed their chain without the grid: 0.0007139); our answer posted (issuecomment-6379669104); recorded in corpus/external-reruns.json; 2026-10-26: MERGED by T. Tao 03:50 UTC (the row 1.9993*, citing [T2026]); the ceiling's printed digit then corrected: the description edited to 0.0007150508, a comment (issuecomment-6421787433) and the one-digit follow-up PR #275
Answered — sent 23 October 2026. A reply to maximusrufus, who opened cert-machine issue 1 offering cross-checks: their from-the-text re-run of the N(6) = 3 search (the openai/math entry our audit could not re-run, no code shipped) and Manvir Jaswal’s earlier one to be noted on that entry as external re-runs, written by us; their explicit AlphaEvolve Ramsey lower-bound graphs accepted for an exact clique/independence decision of our own; our rerun kit offered for the other direction; the two items we both decided agree (C₁₆a, C₁d). (carlostoledo1891/cert-machine issue 1). the issue opened 2026-10-23 15:21 UTC; our reply the same afternoon; they answered 16:28 UTC: pin mub6-certified-rerun at 90607dd4 (its run artifacts unchanged since 7e6ed79f), the Ramsey graphs to come at a fixed commit with sha256s, and they will re-run a few claims from our rerun kit. The dated N(6) note added to the openai/math audit the same day (0b17df38); the graphs and their re-runs wait on them; our closing reply posted the same day with the link to the note (issuecomment-6371185268); 18:24 UTC the Ramsey graphs at maximusrufus/openai-math-replays 4c5524a (Google’s 18 files pinned to google-research 0d94f8c4, SHA256SUMS, their verdicts; R(7,13), R(10,12), R(8,18) not finished); 20:02 UTC a rerun report on three of our records at aa52e8d — twelve register rows re-decided with their own code, three ledgers re-derived, no disagreement — recorded in corpus/external-reruns.json, with two findings (Windows line endings, fixed by .gitattributes; mutations stop at the pin on the ledger path); 2026-10-24 02:32 UTC their three coarse mutations (a duplicated kissing row, moved sum–difference weight, a repeated Heilbronn point) and an offer of one-ulp boundary mutants for the EinsteinArena rows; our report posted 03:13 UTC (issuecomment-6379173543): the Ramsey graphs 16 of 18 CERTIFIED (R(10,12) closed in 77 min), R(7,13) resuming, R(8,18) left open; the boundary mutants accepted; 2026-10-24: the R(7,13) update posted (issuecomment-6383790070): 17 of 18 CERTIFIED, R(8,18) open; 2026-10-24 14:32 UTC their Ramsey cross-check (15 of 15 agree), seven boundary mutants and a C42 rerun note (three defects); all fixed and recorded (ba20083b) and our answer posted (issuecomment-6389814859); 2026-10-26: asked, with no obligation, for a second-party re-run of C82/C86 under the registry's new rule (issuecomment-6421798844)
Answered — sent 22 October 2026. C₃₁ (the binary Chvátal–Sankoff constant): L. Jack's two asterisked rows (Lueker's automaton at h = 9 and h = 10) independently replayed — the automaton rebuilt from Lueker's paper alone in two implementations, calibrated on his Table II, run with witness vectors of our own under directed rounding; both bounds hold; asterisks removed (teorth/optimizationproblems pull request 249). filed at the claimant's own request (e-mail of 2026-10-21); evidence at cert-machine 61aae8eb (certs/lueker-replay.json); label [T2026] on 31a.md; the README's Recent-progress list also edited by our open #242/#243; 2026-10-23: approved by a registry contributor who is not a maintainer (Chessing234), “all good”; not merged; 2026-10-24: JeetuSK0808 posted a third independent replay (their own C from Lueker’s published programs): the state counts equal ours at h = 8, 9, 10, bounds a little looser; our thanks posted (issuecomment-6379668934); recorded in corpus/external-reruns.json; 2026-10-26: T. Tao changed CONTRIBUTING (removing an asterisk takes a second party: a refereed paper, a registration such as Palomar, a maintainer, or an independent confirmation in the thread) and posted the same hold note on #232, #242, #243 and #249; our reply names JeetuSK0808's in-thread C replay as the possible second party (issuecomment-6421793297); 2026-10-27 00:26 UTC: JeetuSK0808 confirmed on the thread that they have no connection to us or to the C31 authors and wrote their replay from Lueker's published programs only (issuecomment-6430610425) — the second party the new rule asks for, if the maintainer accepts it; 2026-10-27 ~03:30 UTC, our thanks POSTED (issuecomment-6433116322), naming the K5/K6 replays on #277/#279; 2026-11-04: maximusrufus's #323 table marks C31 PARTIAL (arithmetic only, the 51M/400M-state automaton runs not replayed); the PR conflicts on constants/31a.md; nothing sent
Answered — sent 20 October 2026. R. Pinho's two asterisked certificates — C₈₆ (the Schur–Siegel–Smyth trace constant, #227) and C₈₂ (the Zhang–Zagier essential minimum, #229) — and the Épi construction the C₈₂ page also asterisks, replayed by two implementations sharing no code with each other or with the claimants, offered as the evidence that removes the three asterisks, in the form pull requests 216 and 230 were accepted. One PR for both because their README lines are adjacent. (teorth/optimizationproblems pull request 242). evidence at cert-machine d9a3942b; merges cleanly with #232 and #243 in either order (test merges); 2026-10-26: T. Tao changed CONTRIBUTING (removing an asterisk takes a second party: a refereed paper, a registration such as Palomar, a maintainer, or an independent confirmation in the thread) and posted the same hold note on #232, #242, #243 and #249; held for a second party; asked maximusrufus to re-run C82/C86 (cert-machine#1, issuecomment-6421798844); 2026-11-04: two second-party replays landed: arhancanli re-ran Pinho's C86 row with code of their own (05:23 UTC), and maximusrufus's #323 (Zenodo 10.5281/zenodo.23938911) marks C86 and C82 REPRODUCED and says our README cell would replace main's newer [Kos2026] 1.8084990*; branch rebased onto main (2ca4846; the C86 cell 1.8117251 (1.8084990*), the Kos2026 row kept) and our reply POSTED (issuecomment-6627410507), disclosing the mutual checks with maximusrufus (#246); 2026-11-04 10:38 UTC: arhancanli also replayed both C82 rows (Pinho's certificate and the Épi construction), with two notes (the Épi value a loose but valid bound; the Épi row names no commit or hash); the row now names them (286afec, BakeLab/Epi-results 97fa6a4, construction.json e85e26fa…, the bytes our replay pinned) and our thanks POSTED (issuecomment-6633371435); each of the three rows now has an independent replay in the thread
Merged — sent 20 October 2026. The C₁c and C₁d step functions replayed by two implementations sharing no code, offered to remove their asterisks; the C₁d bound is printed below its own certificate's exact value, so the PR prints it rounded up (1.4630715826075594), and corrects C₁c's printed decimal. (teorth/optimizationproblems pull request 243). stacked on #232 (adjacent README table rows); evidence at cert-machine d9a3942b; 2026-10-23: approved by a registry contributor who is not a maintainer (Chessing234), “all good”; not merged; 2026-10-26: T. Tao changed CONTRIBUTING (removing an asterisk takes a second party: a refereed paper, a registration such as Palomar, a maintainer, or an independent confirmation in the thread) and posted the same hold note on #232, #242, #243 and #249; then MERGED 03:53 UTC; constants/1d.md lists [CERT2026] twice (…559* and …5594); our comment asks which way (issuecomment-6421793916)
Merged — sent 18 October 2026. The two-law certificate behind C₃c ≥ 1.674894211307116 replayed by two implementations sharing no code with each other or with the claimant, offered as the evidence that removes its asterisk, in the form pull request 216 was accepted. (teorth/optimizationproblems pull request 230). Merged by the maintainer 3.5 hours after it was filed (2026-10-18 05:54 UTC, commit 9938edd4): the asterisk removed, the replay cited on the C₃c page as [T2026b] and in the README's recent progress, and the L2026 row's [T2026] note restored.
Merged — sent 18 October 2026. The four step functions behind the registry's new C₁a and C₁b rows (Atris; EinsteinArena's AgentDiscover and CodexProLong) replayed by two implementations sharing no code with each other or with the claimants, offered as the evidence that removes the four asterisks the maintainer put on them, in the form pull requests 216 and 230 were accepted. (teorth/optimizationproblems pull request 232). 2026-10-26: T. Tao changed CONTRIBUTING (removing an asterisk takes a second party: a refereed paper, a registration such as Palomar, a maintainer, or an independent confirmation in the thread) and posted the same hold note on #232, #242, #243 and #249; then MERGED 03:53 UTC with #243, minutes after the note (our comment on #243 points out the mismatch and the duplicate [CERT2026] row in constants/1d.md)
Answered — sent 15 October 2026. Three of the five bounds in a pull request decided exactly, and two left open for want of a written derivation. (teorth/optimizationproblems pull request 226 (two posts)). The author answered 2026-10-16 with his derivations for 16a and 70a. Both were decided here the same day, from the written derivation and with no code of his run: CERTIFIED. Our follow-up is the last post.
Answered — sent 11 October 2026. Measurements of a kernel patch on 25 real exports from OpenAI's math release, and a request for a configurable worker stack. (ammkrn/nanoda_lib issue 44). The patch it measured was merged the same day (pull request 45) and the issue closed on 2026-10-12; the comment itself has no answer.; 2026-10-12: the maintainer closed it as fixed by #45 (merged 2026-10-11); not re-measured here (no local Lean since 2026-10-20)
Answered — sent 6 October 2026. Two audit records offered to the awesome-ai-proofs registry: the exact re-check of the 4 × 4 matrix-multiplication decompositions (AlphaEvolve rank 48 holds; AlphaTensor rank 47 holds over F₂, fails over Q) and HorizonMath's diagonal-Ramsey certificate, refuted (its λ = 1 pair lies outside the theorem's region; the validator's min for max). (subroy13/awesome-ai-proofs issue 2). Answered 2026-10-17: the maintainer added both records in commit 852a8fac (data/problems/core.yaml, data/problems/carlostoledo1891.yaml; the registry's README now lists the matmul row as ⚑ verified with Claude among the models and a new diagonal-Ramsey row as self-reported · disputed) and closed the issue. Two words softened on their side: the audit event's 'debunked' became 'disputed' and the caveat's 'refuted' became 'contested', pending their source review. Our reply, saying what the record says (REFUTED by an explicit witness; 'disputed' fair until their review), posted 2026-10-17: https://github.com/subroy13/awesome-ai-proofs/issues/2#issuecomment-6235076477 The maintainer answered the same day (issuecomment-6235146613): 'disputed' stays until HorizonMath issue 10 has a comment from its authors, and the issue is to be reopened when it does. On 2026-10-17 HorizonMath issue 10 had no comment.
Merged — sent 6 October 2026. Certificates for C3b, C3c and C71 replayed independently, so the asterisk can come off under the repository's stated rule. (teorth/optimizationproblems pull request 216). Merged by the maintainer on 2026-10-18 (commit ad40c534): the three asterisks are gone, and each constant page (3b, 3c, 71a) cites the replay as [T2026]. The rule it applied was the maintainer's own, from #176: an independent replay removes the marker.
Answered — sent 6 October 2026. K(25) ≥ 197,580 and K(27) ≥ 201,567 checked exactly, and a request for the coordinates of the other dimensions. (Oxelra-AI/Qiushi-Engine-Kissing-Number-Research issue 1 (three posts)). The authors published every remaining configuration within days (2026-10-11 and -12). All nineteen bounds in their paper were then checked pair by pair here, every one holds, and they linked the check beside their results table.; 2026-10-24: the authors (Cherish0925) thanked us for the complete all-pairs verification of all nineteen configurations and updated their English and Chinese READMEs to acknowledge it, linking the report and the programs
Answered — sent 6 October 2026. Erdős #1186 proposed for formalization, with the δ₃ result as context. (google-deepmind/formal-conjectures issue 6882). 2026-10-20: a third party (veljjanoski) took the issue and formal-conjectures merged PR #7467 adding Erdős Problem 1186 the same day; the issue closed as completed
Answered — sent 5 October 2026. A reproducible construction failure of the legacy SandboxEnv in verifiers 0.3.1: no prime-sandboxes release it accepts can build it. (PrimeIntellect-ai/verifiers issue 2775). Closed 2026-10-09 by a maintainer: verifiers v0 was deprecated and removed, and the legacy 0.3.x line will not get a backport.
Answered — sent 3 September 2026. A request to the authors of the 604-point dimension-11 kissing configuration for their vectors, so the one NEEDS DATA row in our ledger can be decided. (vinid/einstein-arena issue 64). The ask is offer-shaped: the certification is already built and waiting on the bytes. Answered 2026-09-07: the maintainer gave the path to the vectors; the two 604-point configurations were decided congruent (a signed coordinate permutation) and the issue was closed 2026-09-08. Two later posts in the same thread: the re-run kit offered (2026-10-05), and a correction of our own figure for the best n = 841 submission, 41,128 exact contacts to 40,992 over its 840 distinct directions (2026-10-06).
Answered — sent 2 September 2026. λ(4) = −L(1,2,3,4) offered as an unusually clean Lean formalization target — six elementary lemmas, exact rational identities, and 2,231 finite cases each carrying a certified enclosure. (teorth/erdosproblems issue 392). Answered 2026-09-30: rainrzk re-certified the whole argument with independent code (erdos510-lambda4-audit), same verdict, three write-up findings folded in; our reply is the last post.
Answered — sent 31 August 2026. The Erdős #290 square-discriminant law as exact integer identities, with a certified bracket for the Galois-density constant — and a correction to my own earlier write-up, in the same comment. (teorth/erdosproblems issue 164). Superseded on the mathematics five days later by arXiv:2609.00104, which proves the liminf exactly; our bracket is now the certified numeric value of that constant rather than one end of a range, and the page says so. Woett answered 2026-09-08 with the theorem; the follow-up with the 1/(1+c) bracket was posted 2026-10-06.
Posted, no reply — sent 5 November 2026. A last update on anthropics/formal-math#36: Anthropic's eth/ proof ported to complexitylib's Lean (762 of 809 files unchanged, 47 edited, PORT.md), so ethIsFalse and the bridge sit in one environment and give ¬ETH on cslib's multitape machine; Lean's six-checker judge, nanoda and leanchecker --fresh accept; what stays open; the port offered as an upgrade path. Sent on Carlos's word. (GitHub, anthropics/formal-math#36). outreach/gh-formal-math-36-chain.md
Posted, no reply — sent 5 November 2026. A follow-up on our issue in Daniel Hawkley's RPI map: beyond RPI-ETH-010, Anthropic's ETHIsFalse now reaches cslib's multitape machine in one Lean; the one version gap left is on OpenAI's side; an RPI suggested. Sent on Carlos's word. (GitHub, thinkthoughts/rpi-index#1). outreach/gh-rpi-index-1-chain.md
Posted, no reply — sent 5 November 2026. A reply in the existing thread with Ramamohan Paturi: Anthropic's proof checked in one Lean through to complexitylib's ETH on cslib's multitape machine; the note (doi:10.5281/zenodo.23966840) and the report; what it does not settle; the target's authors; the definition clause by clause, with one question: does it match ETH as Impagliazzo and Paturi defined it, in particular the (L+1)^e factor. Sent by hand from Carlos's mailbox. (e-mail, a reply in the existing thread (answering a received e-mail; the channel rule)). the text in this session; companion to reports/eth-anthropic-chain.html and paper/eth-chain.pdf
Posted, no reply — sent 5 November 2026. A comment on complexitylib's TM ⇔ RAM issue offering two PRs before opening them: the space-bounded TM ⇒ word-RAM simulation at logarithmic word size (k-SAT, so ETH fails on the log-word RAM; #2027's proof with one step changed, Schlesinger credited) and TM2 steps in a program-independent degree; the checks; the AI and same-author disclosure. Sent on Carlos's word. (GitHub, cslib-community/complexitylib#739). outreach/gh-complexitylib-739-2026-11-05.md; the branches re-checked: corpus/eth-refutation/complexitylib-pr/recheck-2026-11-05
Posted, no reply — sent 5 November 2026. One post: Anthropic's AI proof that the Exponential Time Hypothesis is false runs on a machine Anthropic defined; with AI agents, carried to a standard multitape Turing machine in one Lean; six checkers accept, 9 planted fakes fail; the report with the chain card. Posted by Carlos by hand. (X, @_carlos_toledo_). notes/x/drops/d15-anthropic-chain.txt
Posted, no reply — sent 5 November 2026. The reply under it: what stays open (the textbook match a reading, OpenAI's one version gap, the same author for proofs and checker; replay it) and the 4-page note with its DOI. Posted by Carlos by hand. (X, a reply under @_carlos_toledo_ 2118152759283159493). notes/x/drops/d15-anthropic-chain.txt
Posted, no reply — sent 4 November 2026. The one-post reply under Grigore Roșu's thread on using several models as a review team: what cross-model review misses is right proofs of narrower statements (34 of 242 in OpenAI's math release, passed by every model and kernel), with claimbox named as an early, open attempt at that gap. Posted by Carlos by hand from the X app. (X, a reply under @RosuGrigore's post 2117763822370935037). notes/x/reply-rosu-2026-11-04.txt; the /claimbox/ page has no og:image (a card rendered for the claimbox project in outreach/claimbox-og/).
Submitted, awaiting moderation — sent 4 November 2026. A reply under our comment-24 on the 'announce your results' page: C2, Anthropic's ETHIsFalse implies ETH fails on cslib's standard multitape machine with a binary encoding; with Hawkley's chain both labs' statements reach it; the version seams and the textbook reading stated as open; Zhuang's and complexitylib's native re-proofs named. Posted by Carlos by hand through the blog's form. (ethdiscussion.blog, the 'announce your results' page, a reply to #comment-24). outreach/ethdiscussion-reply-c2-2026-11-04.md; records certs/eth-c2.json, eth-c1.json, eth-cslib-d1.json
Posted, no reply — sent 4 November 2026. A follow-up on anthropics/formal-math#36: the step from FinTM2 on encClauses to a standard machine, named as informal in our earlier comment, is now in Lean (EthBridge.Anthropic.not_eth_of_ethIsFalse, claimbox 235fbfa); how it was checked; what it does not settle; the disclosure. (GitHub, anthropics/formal-math#36). outreach/gh-formal-math-36-c2.md, sent on Carlos's word
Posted, no reply — sent 4 November 2026. One post: the objection to both AI proofs that the Exponential Time Hypothesis is false (each runs on its lab's own machine), that step now in Lean to a standard multitape Turing machine, two kernels each; the textbook match still a reading; the /eth/ chain card. Posted by Carlos by hand. (X, @_carlos_toledo_). notes/x/drops/d14-eth-standard-post.txt (posted from the earlier wording)
Posted, no reply — sent 4 November 2026. A follow-up reply in the thread on the ETH constant: the machine-model step now in Lean to a standard multitape Turing machine, two kernels; what stays a reading marked. Posted by Carlos by hand. (X, a reply under @DimitrisPapail's post 2115451187801514168). notes/x/reply-eth-amplifiers-2026-11-04.txt, text A
Posted, no reply — sent 4 November 2026. A follow-up reply in the thread linking the organizers' announce page: the machine-model step now in Lean to a standard multitape Turing machine. Posted by Carlos by hand. (X, a reply under @rrwilliams's post 2116987964123168822). notes/x/reply-eth-amplifiers-2026-11-04.txt, text A
Posted, no reply — sent 4 November 2026. One post in Portuguese tagging @antihypebr and @fastcompanybra, which covered the ETH claims: the machine step closed in Lean with AI agents, the proofs reaching a standard Turing machine, from Brazil. Posted by Carlos by hand. (X, @_carlos_toledo_). outreach/brasil-eth-comments-2026-11-04.md
Posted, visibility unconfirmed — sent 4 November 2026. A comment in Portuguese under ANTI/HYPE's article on OpenAI's ETH claim, answering the point it left open: both Lean proofs re-checked with two kernels; the machine step closed in Lean with AI agents, Anthropic's statement reaching a standard multitape Turing machine and OpenAI's through Hawkley's bridge; the textbook match and the Lean version gaps marked as readings. Posted by Carlos by hand. (antihype.com.br, comments under 'OpenAI diz que IA derrubou a Hipótese do Tempo Exponencial'). outreach/brasil-eth-comments-2026-11-04.md, C1
Posted, no reply — sent 3 November 2026. The Weight-Space Programming baseline offered to the authors first: the edit decided from the bytes (two tensors, the dose 6), the pre-registered re-run of the unedited Qwen3.5-0.8B under its card's recommended settings (C1 reproduces 7.2%; C3 non-thinking 44–52% against the edit's 48.1), the six side claims decided from their logs; a 24 h window before the public summary. (RikiyaT/lm_understand-logs issue 4). outreach/wsp-authors-issue-2026-11-03.md; records certs/wsp-weights.json, wsp-regrade.json, wsp-baseline.json, wsp-side-claims.json; C2/C4 to be added to the same record. The thread reply and the X post wait for the window (the next morning, decided 14:45 UTC on 11-03).
Posted, no reply — sent 3 November 2026. One reply under the authors' main X post (Takehi, 2117313742891327994): thanks for the release; the edit real as described; the pre-registered re-run — their settings 7.2%, the untouched model under Qwen's non-thinking settings 44–52%; the page linked. Posted BY HAND from @_carlos_toledo_ after the GitHub issue existed. (x.com, reply to rikiyatakehi/status/2117313742891327994). notes/x/reply-wsp-one-2026-11-03.txt (the one-reply version; the four-post chain kept for our own thread). The standalone X post d12 and the ETH post d13 follow the next morning.
Posted, no reply — sent 3 November 2026. The standalone X post on the Weight-Space Programming verification: the edit real; the untouched model under Qwen's own settings 44–52% against the post's 48.1; the 6× mostly settings; the bar-chart card (three arms from the records) attached; the page linked. Posted BY HAND from @_carlos_toledo_. (x.com, @_carlos_toledo_). notes/x/drops/d12-wsp-post.txt + d12-wsp.png (cards-src/cards-wsp-baseline.js). The link carries ?v=2 so X fetched the page's own card (og-wsp.png) rather than its cached landing card.
Posted, no reply — sent 3 November 2026. The reply to Daniel Hawkley's contact-form e-mail (formalize.now) on his ETH bridge RPI-378.3d: the light theorem CERTIFIED on a GitHub runner, the heavy link CERTIFIED on a pod (build, axioms, nanoda with its negative control, leanchecker --fresh), the gaps first (the predicate vs OpenAI's checked statement; the version seam read, not decided), and an offer to measure the seam in his direction. Sent by hand from Carlos's mailbox. (e-mail (answering a received e-mail; the channel rule)). outreach/hawkley-reply-2026-11-03.md; records certs/eth-hawkley-bridge.json, certs/eth-hawkley-heavy.json; his row on /eth/ beside TSavo's. If he accepts the seam offer: pre-register, then the export-and-compare of certs/eth-seam.json in his direction (a GitHub run).
Posted, no reply — sent 3 November 2026. The standalone X post on the ETH bridges: two labs claim ETH is false in two machine models; a third party's Lean bridge from OpenAI's statement to Anthropic's replayed with two kernels and a fresh replay, OpenAI's proof included; one seam stays open. Posted from the session with tools/x.js at Carlos's word ("Send d13"). (x.com, @_carlos_toledo_). notes/x/drops/d13-eth-bridge-post.txt; the link carries ?v=2 so X fetches /eth/'s own card (og-eth.png) rather than the landing card cached from the 11-02 post.
Posted, no reply — sent 3 November 2026. A reply under Giulio Prisco's Metafuturing week post (the column that cited the ETH replay): thanks, and the two updates since — the third-party bridges replayed and certified (/eth/), MIT's weight edit re-run under the model's own settings. Posted by hand from @_carlos_toledo_. (x.com, reply to giulioprisco/status/2116444605491097973). notes/x/reply-prisco-2026-11-03.txt; the column is pinned as recognition row metafuturing-eth-column.
Live, no reply — sent 3 November 2026. The announcement on Mohan Paturi's 'announce your results' page (the organizers' channel; Ryan Williams linked it on X 11-01): three verification results — both formalizations replayed with two kernels and leanchecker; the textbook ETH written once in Lean and refuted by each lab's statement in its own model (51 theorems); the two third-party bridges across the machine-model step (TSavo's, Hawkley's two halves) replayed and certified, the version seam measured and stated as read, not decided. In the format asked: name, affiliation, no coauthors, the disclosures, the link. (ethdiscussion.blog, the 'announce your results' page (comments)). outreach/ethdiscussion-announce-2026-11-03.md; posted by hand, shown as 9:04 am site time on 11-03, comment #24. The e-mail to rpaturi@ucsd.edu SENT 11-03 (row email-paturi-eth-repository-2026-11-03); the one-line reply under Williams's post (notes/x/reply-rrwilliams-2026-11-03.txt) is Carlos's to send.
Posted, no reply — sent 3 November 2026. One reply under Ryan Williams's 'announce your new results' post, pointing to the announcement on the organizers' page: both formalizations replayed with two kernels, the textbook ETH written once in Lean and refuted by each statement in its own model, the two third-party bridges replayed and certified. Posted by hand from @_carlos_toledo_. (x.com, reply to rrwilliams/status/2116987964123168822). notes/x/reply-rrwilliams-2026-11-03.txt; companion to ethdiscussion-announce-2026-11-03 and email-paturi-eth-repository-2026-11-03.
Posted, no reply — sent 3 November 2026. The replay of TSavo's ETH bridge told to its author: CERTIFIED by Comparator with Lean's kernel and nanoda on a GitHub runner, the lakefile amendment the run had to declare, and the version seam measured term by term (the statement the same kernel term up to a binder name; 308 of 2,689 reachable constants differ between the two Mathlibs); Hawkley's bridge the other way round mentioned. (TSavo/eth-bridge issue 1). outreach/tsavo-issue-2026-11-03.md; records certs/eth-tsavo-bridge.json, certs/eth-seam.json. Posted from the session with gh at Carlos's word.
Posted, no reply — sent 3 November 2026. A public flag for Daniel Hawkley on his registry, in its own format (third-party report vs local reproduction): both edges replayed and CERTIFIED — RPI-ETH-010 on a GitHub runner (Comparator with Lean's kernel and nanoda), RPI-ETH-008 on a CPU pod (build, axioms, nanoda with its negative control, leanchecker --fresh); the records to attach; the machine-model reading and the seam offer; in case the e-mail of 11-03 did not arrive. (thinkthoughts/rpi-index issue 1). outreach/hawkley-issue-2026-11-03.md; companion to email-hawkley-reply-2026-11-03 (thinkthoughts/math has issues off). Posted from the session with gh at Carlos's word.
Posted, no reply — sent 3 November 2026. The two-line follow-up to Reg Saddler (@zaibatsu, The Build) under his ETH column: the third party's bridge the other way round replayed with two kernels (it holds), and MIT's weight-space programming re-run under Qwen's own settings; an offer to walk him through either. Posted by Carlos by hand from the X app. (X, a reply under Saddler's column (conversation 2115840407095439365)). notes/x/reply-zaibatsu-2026-11-03.txt; posted 14:51 UTC; the first reply (11-02, 2117396073526227039) answered his correction. His column is recognition row the-build-eth-column.
Posted, no reply — sent 3 November 2026. The three-post reply under the critic's post on MIT's Weight-Space Programming (@dummerspast39, 1,520 likes, 162k impressions; pinned in corpus/wsp/critic-2117416640132366570.json): most of his numbers hold against the released bytes (93.1% cut, 7.2% under their settings; 45.6% / 51.7% with no edit under Qwen's settings, his 47 inside; 2 tensors; Frogger/Freeway, 876, 20× PPO, two games lost, sycophancy), two refuted ('test answers' — 3,680 practice answers; 'one run replayed' — 1,024 sampled episodes), the termination reading. Posted by Carlos by hand from the X app. (X, three replies under the critic's post, each a reply to the previous (conversation 2117416640132366570)). notes/x/reply-critic-2026-11-03.txt + .md; posted 22:41–22:42 UTC (2117748912534499369, 2117748973574529300, 2117749238050513045).
Public, no reply — sent 3 November 2026. A public compute ask: two posts tagging @PrimeIntellect with the Verify Gym chart (seven open models below exact bisection, every number from certs/verify-gym-scorecard.json) asking compute for one pre-registered training run (Qwen3.5-9B, GRPO, US$500 cap, the stopping rule, a tolerance-reward twin; published on the Hub whichever way it falls). Posted by tools/x.js on Carlos's word. (X, a two-post thread from @_carlos_toledo_). the X thread with the Verify Gym chart; the second post 2117753359729844651; posted 22:58 UTC.
Posted, no reply — sent 3 November 2026. The one-post reply under Pawel Huryn's post on the Weights story (82 likes): the same reading from the bytes, the baseline under Qwen's own settings (45.6% / 51.7%), the dose tuned on 3,680 practice answers, the records link. Posted by Carlos by hand from the X app. (X, a reply under @PawelHuryn's post 2117639929463197885). notes/x/reply-huryn-2026-11-03.txt; posted 23:01 UTC by Carlos.
Posted, no reply — sent 3 November 2026. The one-post reply under @rryssf's loop-fix thread: the direction is reversed, not subtracted (W − 6·u(uᵀW), the 6 to three decimals), and the gain is termination (35 of 500 → all right; 303 → 241), the records link. Posted by Carlos by hand from the X app. (X, a reply under @rryssf's post 2117523275266101287). notes/x/reply-rryssf-2026-11-03.txt; posted 23:01 UTC by Carlos.
Posted, no reply — sent 3 November 2026. The one-post reply to @miriamgonp's 'compared to what?': the untouched model under Qwen's own settings (45.6% / 51.7%) against the edit's 48.1; pre-registered, exact grading, texts released; the edit real, the 6× mostly a settings effect. Posted by Carlos by hand from the X app. (X, a reply under @miriamgonp's post 2117686029507309778). notes/x/reply-miriamgonp-2026-11-03.txt; posted 23:02 UTC by Carlos.
Posted, no reply — sent 3 November 2026. The one-post reply under Runchu Tian's steering critique (42 likes): steering, with the direction reversed, not deleted (the 6 to three decimals), and the gain termination; the records link. Posted by Carlos by hand from the X app. (X, a reply under @Runchu_Tian's post 2117633356464902492). notes/x/reply-runchu-2026-11-03.txt; posted by Carlos 11-03 (Carlos confirmed; posted ~23:10 UTC).
Open, no comments — sent 3 November 2026. The issue on Jason Davies's repository telling him his classification of the minimum universal sets of MacMahon cubes was replayed and certified twice here with no shared code — the 300 released witnesses re-built with our own geometry, the ten theorems through Lean's kernel and nanoda with our own axiom report — with the two records, the statement reading, what is not claimed, and the page. Posted with gh on Carlos's word. (jasondavies/macmahon-min-universal-sets, an issue). outreach/davies-issue-2026-11-03.md; the page carlostoledo.co/reports/macmahon.html went live minutes before; posted ~23:45 UTC.
Posted, no reply — sent 30 October 2026. One post on X: both claimed ETH refutations pass two independent kernels and a fresh replay; each statement refutes a textbook ETH written in Lean; whether that Lean ETH is the textbook one is read, not decided; the /eth/ link, with the disclosures (tools built with Claude; one claim is Anthropic’s). (X, a reply under Dimitris Papailiopoulos’ post on the galactic ETH constant). posted by hand from @_carlos_toledo_ (the API refuses replies to posts that do not mention the account); the url is the post replied to; the reply’s own id is not yet recorded.
Posted, no reply — sent 30 October 2026. A reply to maximusrufus's fixes for our C_16 replay observations (maximusrufus/c16-bgw-certificates@0c57070): the certifier scripts now in the repository; both float fields checked exactly as the nearest doubles on the correct side of their rationals; the rationals byte-identical to those replayed, so the verdicts stand (lower certified, upper finite core certified with analytic steps read); the asterisks left to the maintainers. (teorth/optimizationproblems pull request 246). outreach/c16-246-followup-2026-10-30.md; the check never ran the claimant's code.
Live, no reply — sent 29 October 2026. TSavo’s Lean bridge (OpenAI’s Claim → MainResults.ETHIsFalse, TSavo/eth-bridge @ 34f9ca20) replayed and certified by two kernels, with its two gaps named (the README’s lakefile cannot run Comparator; the two Lean versions compose by the source text, not one kernel run); and their question answered, whether MainResults means ETH: two independent readings say ETHIsFalse is literally s₃ = 0, and our generic Lean ETH equals Anthropic’s s by rfl. (anthropics/formal-math issue 36). certs/eth-tsavo-bridge.json (run 40789891989), certs/eth-bridge.json, the readings; /eth/ linked; disclosures included
Live, no reply — sent 29 October 2026. A follow-up offering the model-generic ETH (ETHBridge/Generic.lean, MIT) as a fixed target for later claims: ETH and #ETH stated once, ¬ETH and ¬#ETH proved from each lab’s statement in its own model (Anthropic’s #ETH on the formulas MainTheorem speaks of), 51 theorems each accepted by Lean’s kernel at build, Lean’s kernel in Comparator and nanoda; and the join’s version seam measured: the statement is the same kernel term up to a binder name, but ℝ’s arithmetic differs between Mathlib 0df444a3 and d13f23b7, so no single kernel has checked the two statements are one proposition. (anthropics/formal-math issue 36). certs/eth-bridge.json (run 40947192141), certs/eth-seam.json (run 40947568989); disclosures included; v2, with the seam paragraph
Filed, no reply — sent 28 October 2026. Answers to the TCS community form on the two claimed refutations of ETH (organizers Impagliazzo, Paturi, Williams): how to organize the examination (proof checks, statement readings, the informal mathematics kept apart), making the argument accessible, the consequences in three registers, and a virtual meeting (yes; two two-hour sessions). It reports both Lean proofs checked by two kernels, the two readings, and the Lean bridge (one textbook ETH, each lab’s statement proved to refute it in its own model), with the disclosures: tools and proofs written with Claude, one claim is Anthropic’s, no affiliation with either lab. (the TCS Community Feedback about ETH form (Google Forms; responses reviewed by the organizers, not public)). submitted 2026-10-28 ~23:20 UTC; links /eth/ (unlisted), certs/eth-kernel.json, corpus/eth-refutation/bridge/; the answers as sent are kept locally in notes/tcs-form-answers-2026-10-28.md (the optional blog comment was not posted)
Live, no reply — sent 28 October 2026. A short comment for readers checking the formal side of the two ETH claims: both Lean developments replayed with Comparator under Lean’s kernel and nanoda (both check against their own statements, standard axioms only); OpenAI’s Lean defines no ETH, so the textbook ETH written once in Lean and each statement proved to refute it in its own lab’s machine model, the step between machine models informal for both; with the disclosures (tools and proofs written with Claude, one claim is Anthropic’s, no affiliation with either lab). (ethdiscussion.blog, the organizers’ public discussion page (comments moderated)). posted 2026-10-28 ~23:30 UTC; links /eth/ (unlisted); the text as sent is in notes/tcs-form-answers-2026-10-28.md (local). Check whether it appears; then set the status to live, no reply.
Posted, no reply — sent 27 October 2026. The K5 Ramsey-multiplicity certificate (C₈₉b ≤ 0.0016870052, J. SK's 192-block step graphon) re-derived by two implementations sharing no code with each other or with the claimant's evaluators: the density equals the fraction the page states, the printed bound is it rounded up; five controls — offered as the second party the registry's rule of 2026-10-26 asks for. (teorth/optimizationproblems pull request 277). certs/graphon-replay.json at d813a99b; the page /reports/optconst-queue.html#graphons; the claimant is the second party on our #249, so this is the reciprocal confirmation; a README nit noted (1,248 pairs moved, not all 18,528 entries)
Posted, no reply — sent 27 October 2026. The K6 Ramsey-multiplicity certificate (C₈₉c ≤ 0.7422548616·2⁻¹⁴, J. SK's Z₂¹⁰ weight-class step graphon) re-derived by two implementations sharing no code with each other or with the claimant's evaluators: the density × 2¹⁴ equals the fraction the page states, the printed bound is it rounded up; the perturbation and half-graphon controls — offered as the second party the rule asks for. (teorth/optimizationproblems pull request 279). certs/graphon-replay.json at d813a99b; the page /reports/optconst-queue.html#graphons
Posted, no reply — sent 27 October 2026. maximusrufus's C₁₆ enclosure (2.1562247706 ≤ C₁₆ ≤ 2.1562256466) re-decided from the published certificates by two implementations sharing no code, the claimant's checkers read as text and never run: the lower end holds exactly; every finite step of the upper end holds on all 84 boxes against the printed digits (the boxes support 2.1562256458), its analytic steps read and re-derived — offered as the second party the registry's rule asks for, and as the reciprocal check of their reruns of ours. (teorth/optimizationproblems pull request 246). certs/c16-replay.json at f4ee2715; /reports/optconst-queue.html#c16; four observations noted (the bound the boxes support, the checkers' tolerance, the unpublished certifiers, two float slips)
Posted, no reply — sent 27 October 2026. The K4 Ramsey-multiplicity certificate (C₈₉ ≤ 0.0301388794, J. SK's 3,840-block step graphon) re-derived by two implementations sharing no code (a C kernel on a rented CPU pod, every block; an exact JavaScript second implementation by orbits) agreeing on all 3,840 blocks: the density is the fraction the page states, the printed bound it rounded up; offered as the second party. (teorth/optimizationproblems pull request 255). certs/graphon-k4.json at f4ee2715; /reports/optconst-queue.html#graphon-k4; the README nit noted ([Kos2026] shown as C₈₉'s best, not the page's smaller [SK2026])
Posted, no reply — sent 27 October 2026. J. SK's R(3,33) ≥ 241 circulant certificate (Zenodo 23552014, linked from the C₁₇b page) re-decided with our own code: the graph rebuilt from the printed connection set, triangle-free, and no independent 33-set by an orbital branch-and-bound (one root by transitivity, 31 stabilizer orbits, 9 minutes on 8 threads); a SAT second path closed 22 of the 31 cubes with checked proofs. (teorth/optimizationproblems pull request 252). certs/ramsey-ledger.json (the outside row) at f4ee2715; /reports/ramsey-graphs.html#other-graphs
Filed, no reply — sent 26 October 2026. C₈₄b: the chain's ceiling printed rounded up (0.0007150508) instead of truncated (0.0007150507), a one-digit follow-up to #257 (teorth/optimizationproblems pull request 275). the digit from certs/sumproduct-ledger.json (d5e86354)
Filed, no reply — sent 23 October 2026. zeta23 (anthropics/formal-math), the ξ′ side: the quartic window 8.85·10⁻⁷ below its own family's optimum; the degree-6 window v₆ and D1trunc 15 give 0.86864150 / 0.93432075 against the formalization's 0.86864017 / 0.93432008 (+1.33·10⁻⁶), with the optimality certificate over even polynomial windows of degree ≤ 20, the ζ calibration to eighteen digits, what AtOne.lean needs, and the abstract's 0.8362 as a truncation (anthropics/formal-math issue 30). a separate matter from the law-file thread (#8); every number a decision on claimbox afd776c's certificates and re-derived by the paper's generator (a third implementation); the e-mail to the paper's authors was dropped (e-mails off), its content here; 2026-10-23 a follow-up comment linked the companion paper now live (https://github.com/anthropics/formal-math/issues/30#issuecomment-6357042052)
Posted, no reply — sent 23 October 2026. the reply to Leandre Jack's e-mail of 2026-10-21 asking for the C₃₁ replay: both rows replayed and holding, the h = 9 and h = 10 numbers, the observation on his λ (1.5·10⁻¹¹ and 1.1·10⁻⁷ above ours), PR #249, the page, two questions (his state order; a Zenodo deposit of our vectors) (e-mail, a reply to his). sent by Carlos Toledo by hand; the one e-mail the channel rule allows — an answer to one received
Filed, no reply — sent 23 October 2026. google-deepmind/cryptids: the finite layer re-checked at 664cd039 from the bytes by two implementations sharing no code with verify.py (143 of 152 checks hold) and both comparator configurations passed under Lean’s kernel and nanoda; six notes — the riemann_104 check never runs riemann_120 (we ran it 89,775,610 steps: no halt), the checkpoint table’s steps are the 179th/210th/879th/1,721st root entries (the selection rule unpublished), “non-halting transitions” counted two ways (785/759 vs 784/758 cells), proof-file digests recorded and compared to nothing, statements checked by substring, three smaller prints (google-deepmind/cryptids issue 14). their CONTRIBUTING invites oversights as issues; items 1–3 re-run independently before posting; text in outreach/github-2026-10-23.md; no PR offered (it would need Google’s CLA)
Posted, no reply — sent 22 October 2026. zeta23 (anthropics/formal-math): the bandwidth-one ceiling's row certificate re-decided from LawN256.lean's 256 integers by two programs sharing no code with Lean (three claims hold; the CUE containment 124/131); the request for the law file cert_N256_blk_b128m.json behind EnclOK joined (anthropics/formal-math issue 8, comment). a comment on the open request of 2026-08-12 (issues #8 and #14 already asked; no author reply in two months), not a new issue; evidence at claimbox b37d980; the companion paper (riemann-finite-layer) waits on the XiPrime pins before its push
Filed, no reply — sent 20 October 2026. AlphaProof Nexus: every published Erdős proof and the corrected #741(i) replayed under Comparator against formal-conjectures' statements and two kernels (all hold), with four notes on the OEIS results: A382590's statement counts prime factors with multiplicity and is degenerate; earlier proofs on record for A325046, A382590 and A237271; A237271 defined by an already-proved characterization; 38 of 44 OEIS proofs published. (google-deepmind/alphaproof-nexus-results issue 4). filed on request; evidence at cert-machine 7b13a32f
Open, no comments — sent 15 October 2026. The finite core of the Bandeira 0.2(a) disproof re-decided with our own certificate (it holds), and the two gaps at its declared boundary named. (Oxelra-AI/Bandeira-0.2a-open-source issue 1 (two posts)).
Live, no reply — sent 15 October 2026. Both constructions for C1a and C1b re-decided exactly; the bounds hold. (teorth/optimizationproblems pull request 225). The pull request was merged on 2026-10-18 and the maintainer then marked both bounds with the asterisk, as replayed only by the submitting team's own checker (commit 3010f7ed); the comment is not cited.
Live, no reply — sent 15 October 2026. The C3c lower bound decided with interval entropies at 128 bits; it holds. (teorth/optimizationproblems pull request 221). Merged on 2026-10-18 with its asterisk kept; the replay was then offered as pull request 230 the same day, decided a second time by an implementation sharing no code with the first.
Live, no reply — sent 15 October 2026. A record package for the de Bruijn–Newman constant read file by file: what an outside party can and cannot decide from it. (teorth/optimizationproblems pull request 210). Merged on 2026-10-18 with its asterisk, and every row of the constant since 2021 now carries one as not independently replayed — consistent with the comment's reading; the comment itself has no reply.
Open, no comments — sent 6 October 2026. The diagonal-Ramsey certificate of Appendix A.3 refuted: its λ = 1 pair lies outside the region Theorem 14 requires, and the validator accepts it by taking a min where membership needs both inequalities. (ewang26/HorizonMath issue 10). The awesome-ai-proofs registry keeps its entry "disputed" until this thread has a comment from the authors.
Closed, no comment — sent 6 October 2026. K(18) ≥ 8,358 checked exactly from the published data, and the dimensions 25–31 with it. (alexlegeartis/KissingNumbers issue 2). closed by the owner as completed on 2026-10-23, without a comment; no commit to the repository since 2026-09-27
Open, no comments — sent 6 October 2026. K(25) ≥ 197,058 checked exactly; in dimension 31 the stored added points differ from the README. (k-nic/Leech_lifting issue 1).
Open, no comments — sent 6 October 2026. One table row needs an update: the circles-in-a-rectangle solution (n = 21), read exactly, has 44 overlapping pairs and is rejected by today's verifier. (togethercomputer/EinsteinArena-new-SOTA issue 14).
Live, no reply — sent 6 October 2026. The 600-step Erdős construction re-decided in exact arithmetic, in a thread asking whether the published score can be verified. (test-time-training/discover issue 19). The thread had been closed since July; the comment answers its question.
Open, no comments — sent 6 October 2026. δ₃ = 117/2192 claimed optimal for k = 3 of Erdős #1186, and why the exact value of the published δ₄ blocks the next step. (incrediblecrab/erdos-1186 issue 1). 2026-10-23: the repository incrediblecrab/erdos-1186 no longer exists (404), so the issue is gone with it
Open, no comments — sent 6 October 2026. Remark 17's iteration checked against Theorem 14 on all of (0, 1] in interval arithmetic: it holds, given the paper. (snorin239/RamseyLean issue 1).
Open, no comments — sent 6 October 2026. The hot spots conjecture (Rauch, 1974) proposed for formalization, with a certified family of trapezoids. (google-deepmind/formal-conjectures issue 6874).
Live, no reply — sent 6 October 2026. The Hankel-determinant method measured past ζ(5) by a separate engine: it does not reach ζ(7). (mo271/Zeta5 issue 3).
Open, no comments — sent 5 October 2026. The Time Horizon 1.1 logistic fits re-derived in standard-library Python, each optimum certified by Krawczyk's method instead of refitted. (METR/eval-analysis-public issue 43).
Open, no comments — sent 5 October 2026. After the λ(4) audit, three more rows offered for re-running, from the re-run registry. (rainrzk/erdos510-lambda4-audit issue 1).
Open, no comments — sent 5 October 2026. The 604-point kissing configuration in dimension 11 certified in exact arithmetic and congruent to the EinsteinArena one; two more configurations decided. (dualverse-ai/station_data_v2 issue 2 (two posts)).
Open, no comments — sent 5 October 2026. The counterexample library decided case by case, and the one case whose verdict depends on its reading (feasible Picard steps for DPP likelihood). (suvrit/count-ex-machina issue 1).
Live, no reply — sent 5 October 2026. A third-party report on Anand's ζ(7) preprint confirmed with exact values: I_out in Table 5 does not follow from (59). (gmDevi/zeta-7-21-lean issue 1).
Public, no reply — sent 5 October 2026. A partial proof claim for Erdős #1186: δ₃ = 117/2192 for three-term progressions, with an exact lower-bound certificate. (the proof claims of erdosproblems.com/1186). Accepted by the moderators and shown on the problem from 2026-10-06; no comment on it by 2026-10-17.
Open, no comments — sent 16 September 2026. Erdős #1 made effective: the explicit sets and their certificates, offered to the project tracking the problem. (tadamcz/erdos1 issue 2).
Public, no reply — sent 16 September 2026. Erdős #1 made effective: explicit sets for which the conjecture's bound fails at stated sizes, with the certificates. (the erdosproblems.com forum, thread 1). Visible (dated 14:25 on 16 Sep 2026). One post came after it, building on the thread's earlier suggestion rather than answering this one.
Live, no reply — sent 3 September 2026. Both ends of Erdős #1038: per-degree theorems on the supremum side, then a certified lower bound inf ≥ 1.828 with no tail estimate and no assumed minimizer. (teorth/erdosproblems issue 179 (three comments)). The second comment was edited after posting to fix rendering: GitHub's KaTeX rejects \\operatorname and renders \\, as a visible comma. A third comment (2026-10-06) corrected our own figure on #1038; nobody has answered any of the three.
Public, no reply — sent 3 September 2026. The same infimum result, rewritten for the forum's own rules — derivations pushed to the linked PDF because the site forbids posting partial proofs in full. (the erdosproblems.com forum, thread 1038). Visible on the thread (dated 14:39 on 3 Sep 2026) and still its last post on 2026-10-17.
Public, no reply — sent 26 August 2026. A correction to a GPT-published constant on Erdős #852 — refuted at its 11th significant digit (its 12th decimal place), certified replacement attached. (the problem's discussion thread on erdosproblems.com). It cleared moderation and stands visible (the thread dates it 00:06 on 26 Aug 2026, and it is still the last post there). The thread as it stands is pinned in this repository as evidence bytes. Visible is not endorsed: nobody has answered it, no author has amended anything, and clearing a moderation queue is not peer review and not an independent rerun.
Public, no reply — sent 26 August 2026. The certified table of λ(n) for Chowla's cosine problem (#510), with the λ(4) result. (the erdosproblems.com forum). Visible on the thread since it was posted (dated 21:32 on 26 Aug 2026); it was first seen there on 2026-10-06, because the watch had been reading the problem page, where comments do not render. Still the last post on 2026-10-17.
Filed, no reply — sent 5 August 2026. An independent confirmation of the computational appendix of a claimed proof of Erdős #1038 — all 30 printed decimals verified by a different route, Krawczyk rather than bisection. (Pengbinghui/pipeline-math issue 5, the claiming authors' own repository). To my knowledge still the only independent verification of any part of any of the three claimed proofs of that problem.
Posted, no reply — sent 4 August 2026. An evaluation note on a public automated-alignment sandbox whose authors invited stress-testing. (safety-research/automated-w2s-research issue 2).
Still in the moderation queue — sent 4 August 2026. A note on Erdős #290, whose constant's decimal expansion is also an OEIS submission. (erdosproblems.com and OEIS). Not visible on erdosproblems.com/forum/thread/290 on 2026-10-17: five posts, none of them this one.
Status words mean exactly what they say and nothing more: public, no reply — visible to everyone, answered by nobody · filed, no reply — received by the other party's tracker, unanswered · posted, no reply — published where it was aimed, unanswered · open, no comments — an issue nobody has responded to · live, no reply — a comment visible in the thread, unanswered · posted, visibility unconfirmed — submitted, and we have not verified it appeared · submitted, awaiting moderation — in a queue, not yet visible · still in the moderation queue — submitted and confirmed not yet visible · answered — the other party replied in the thread; what came back is in the note · reviewed, not merged — a reviewer who is not a maintainer answered in the review; nothing merged · merged — accepted into the other party's repository · closed, no comment — the other party closed it without a reply. Last checked 4 November 2026.
Filed is not accepted; posted is not replied. Third parties have re-derived results on this site seven times (above): five with code of their own, sharing none with ours, and two with the tools that wrote the record; none of it has been peer-reviewed. That is the plain state of it, and it is why the pages ship their own falsifiers rather than asking for trust.
Traffic in the other direction has somewhere to go now: the claims desk takes a claim and answers it in public, whichever way it falls. 131 claims have been decided so far, and zero were sent by somebody else — a number this site publishes while it is still zero.
working together
What a collaboration or a hiring process can check
Open to collaboration — an independent audit of a release or a registry, a benchmark review, a certified decision product for an operation with a number to defend — and to roles in evaluation and verification. The four artifacts below were built to be re-run rather than read; every number in them is taken from a ledger at build time, and a number that stops holding refuses this page. The conventional CV is available on request.
METR’s time horizon, re-derived as certificates. 44 of 44 fits with the optimum proved unique in a box below 10⁻¹⁰ on METR’s own files; the printed coefficients are the box’s rounding for 22 of 23 models; the post-2023 doubling time re-derives as 128.740 days against the printed 128.744. The page.
blind-spot, an RTL mutation task under Inspect and verifiers. 400 pooled mutants, 892 submissions scored three ways with 0 disagreements; 3 frontier models, 180 rollouts, every one re-scored offline with 0 disagreements. The instrument · the Inspect task.
GSM8K’s answer key, re-decided. 4,282 test and 23,716 train calculator annotations evaluated from the expressions they print; 2 test and 24 train keys print a step that does not hold as printed. The page.
Three verifier-graded environments on the Prime Intellect hub.blind-spot, break-the-grader and lattice-claims, no answer key in any of them: a kill is simulated, a lattice claim is decided exactly, a grader is broken or is not. At its last control build (git 7ce2f9f8) the repository ran 181 batteries, 181 of them green. break-the-grader · the repository.
decided
exact arithmetic backs it
computed
float, or a number someone printed; nothing decided it
why these numbers stand as they do
computed — the doubling time METR printed; nothing here decided it
absent by choice
What this page does not contain
No employment history, no degrees, no years-of-experience figure, no self-rated skills. Each of those is a claim a reader would have to take on trust, and putting them beside claims that can be re-run devalues the second kind. If a process needs a conventional CV, ask and you will get one.
method
How these pages are made, since it bears on how fast they appear
The mathematics, the design of every check, and the decision about what may be claimed are mine. The writing and much of the implementation are done with AI assistance, under the discipline this site describes: a screen may only prune, a gate counts only once it has been shown to go red on a broken copy, and every page recomputes its numbers from the records at build time — a build that drifts refuses to ship. The output rate is a consequence of that arrangement, and saying so seems better than letting a reader wonder.
The code and the checks on it share one author, so they rule out slips but not a shared misconception. An independent recomputation of any result here — in whatever you already trust — is the thing this site most wants, and a refutation gets published like any other result, with the name of whoever found it if they want it there.
contact
One address, for everything
carlos@carlostoledo.co — corrections, questions about a step, collaboration, hiring. A message that names the page and the one step it doubts can be answered properly; a general introduction usually cannot. For a hiring process, the section above is the checkable half of a CV; the conventional one on request.