About

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.

• Audits of machine-generated mathematics (35). 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 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, since 2026-10-09, by an adversarial read of the code, counted apart; the erratum of that date is on the machine page.

Credited elsewhere: what registries, claimants 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)
• 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)

• 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).
• Independently re-derived, no shared code — 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) (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).
• Independently re-derived, no shared code — 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 (13 of 66), then everything else, newest first.

• 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)
• 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.
• 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
• Merged — sent 6 October 2026. This repository proposed for the list's peer-review and verification section. (Omni-Scientist/Awesome-AI-Scientist pull request 5). Merged 2026-10-06.
• 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.

• 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)
• Reviewed, not 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
• Reviewed, not merged — 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
• 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. 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)
• Reviewed, not 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
• 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
• Filed, no reply — 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).
• 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. Problem 60 (no five points on a sphere): every point set in the thread re-decided in exact integer arithmetic. (google-deepmind/alphaevolve_repository_of_problems issue 6).
• Live, no reply — sent 15 October 2026. Problem 59 (no isosceles triangles): both 58-point sets decided exactly; zero isosceles triples, and both maximal. (google-deepmind/alphaevolve_repository_of_problems issue 10).
• Live, no reply — sent 15 October 2026. Problem 61 (ring loading): the m = 14 and m = 15 instances decided over every sign pattern, under both index ranges. (google-deepmind/alphaevolve_repository_of_problems issue 12).
• Live, no reply — sent 15 October 2026. Problem 42 (sum-difference constant): the finite parts of the note decided by exact sumsets. (google-deepmind/alphaevolve_repository_of_problems issue 5).
• Live, no reply — sent 15 October 2026. WOWII 353: the 25-vertex counterexample decided from the archive's definitions. (google-deepmind/formal-conjectures issue 7304).
• Live, no reply — sent 15 October 2026. WOWII 360: the 41-vertex counterexample decided under both readings of the ½. (google-deepmind/formal-conjectures issue 7305).
• Live, no reply — sent 15 October 2026. WOWII 373: the 150-vertex counterexample decided. (google-deepmind/formal-conjectures issue 7306).
• Live, no reply — sent 15 October 2026. WOWII 396: the 39-vertex counterexample decided. (google-deepmind/formal-conjectures issue 7308).
• Live, no reply — sent 15 October 2026. WOWII 395b: the 15-vertex counterexample decided by exhaustion. (google-deepmind/formal-conjectures issue 7330).
• Live, no reply — sent 15 October 2026. The pull request for WOWII 353: the witness decided independently, with a pinned copy of it. (google-deepmind/formal-conjectures pull request 7310).
• Live, no reply — sent 15 October 2026. The pull request for WOWII 396: the witness decided, with a note on a unique mode. (google-deepmind/formal-conjectures pull request 7320).
• Live, no reply — sent 15 October 2026. The pull request for WOWII 360: the witness decided under both readings. (google-deepmind/formal-conjectures pull request 7321).
• Live, no reply — sent 15 October 2026. The pull request for WOWII 373: the witness decided. (google-deepmind/formal-conjectures pull request 7322).
• Live, no reply — sent 15 October 2026. The pull request for WOWII 395b: the witness decided, with a note on a hypothesis the archive does not carry. (google-deepmind/formal-conjectures pull request 7337).
• 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).
• Live, no reply — sent 6 October 2026. An independent check of the C42 half of a pull request, read as exact rationals. (teorth/optimizationproblems pull request 184).
• 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 12th significant digit, 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 23 October 2026.

Filed is not accepted; posted is not replied. 7 results on this site have been independently re-derived by a third party sharing no code (above); none 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 have been decided so far and 0 of those was sent by somebody else — a number this site publishes while it is still zero.

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.74 days against the printed 128.744. The page.
• blind-spot, an RTL mutation task under Inspect and verifiers. undefined pooled mutants 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. The repository runs 160 batteries at every control build. break-the-grader · the repository.

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.

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.

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.