Carlos Toledo · about
Not correct. Checkable.
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.
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, or an impossible number — none by reading code.
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
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:
- Public, no reply — sent 27 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 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.
- 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. (an issue on 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. (an issue on that repository).
- Submitted, awaiting moderation — sent 4 August 2026. A note on Erdős #290, whose constant's decimal expansion is also an OEIS submission. (erdosproblems.com and OEIS).
- Live, no reply — 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. A follow-up comment is written and unsent.
- 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 (two comments)). The second comment was edited after posting to fix rendering: GitHub's KaTeX rejects \\operatorname and renders \\, as a visible comma.
- Open, no comments — 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).
- Posted, visibility unconfirmed — 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). The site queues comments for moderation and I have not confirmed this one visible.
- Still in the moderation queue — sent 2 September 2026. A note on Chowla's cosine problem (#510) and the λ(4) result. (the erdosproblems.com forum). Checked by tools/sweep-claims.js, which watches for it appearing.
- Open, no comments — 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.
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. Last checked 3 September 2026.
Filed is not accepted; posted is not replied. No result on this site has yet been reproduced by anyone else, and 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. 18 have been decided so far and 0 of those was sent by somebody else — a number this site publishes while it is still zero.
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. A message that names the page and the one step it doubts can be answered properly; a general introduction usually cannot.