Carlos Toledo
About · Carlos Toledo · Brazil

I work on computer-assisted proof and validated numerics.

The job is narrow, and it is 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, and contraction arguments of the radii-polynomial and Krawczyk kind. I work alone, from Brazil, and I travel when there is a reason to.

What the work is

The notes on this site are the work, not a summary of it. Each states what it certifies, what it assumes, and what it will not claim; each ships the program that produced its numbers, and several run the argument live in the page. Where the method fails, the note says which step failed rather than loosening a tolerance until something turns green. The tempo is part of the method: when a frontier paper ships a machine-checkable claim, an independent re-verification here typically exists within days — the Maxwell counterexample paper appeared on 29 July 2026 and its 24 equilibria were certified here on 4 August. Six of the notes on the reports page:

NoteWhat it is
Verification lane Six AI-claimed mathematical results from a public claim database, each re-checked from scratch in independent arithmetic with a planted bug proving the check can fail: five confirmed on the layer checked, one PARTIAL — its machine-checkable fragment confirmed in full, its analytic core not audited, and the note says so rather than smoothing it away.
Erdős #290 The Galois data van Doorn's problem page asked for, computed in plain Node.js over exact rationals rather than in Sage or Magma: three unresolved degrees pinned exactly, two more found beyond the published range, and the pattern behind them proved rather than observed.
Wardrop reproduction An independent reproduction of Bakaryan, Aoun, de Lima Ribeiro, Hovakimyan and Gomes, Distributed Hessian–Riemannian flow for multi-population Wardrop equilibrium, AIMS Mathematics 11(5) 2026. Three scenarios, three different outcomes: one refused, one solved exactly over rationals, one certified by a Krawczyk argument.
Congestion mean-field game Existence, local uniqueness within the even subspace, and strict positivity of the density, certified in outward-rounded interval arithmetic. It ships a single-file verifier: Python standard library, no dependencies, a couple of seconds.
Price formation with a stock constraint The water-value problem on a scenario tree — what a unit of stored energy is worth today given that spending it now means not having it later. Certified by zero-gap linear programming duality, where the sign of the gap is what carries the argument.
Verifying a model's mathematics A candidate answer goes in; a certificate or a refusal comes out, with no language model anywhere in the checking path. Formal proof systems cover discrete logic well; bounds, positivity, existence and stability need a numerical certificate instead.

The standard these are held to

Every number is produced by a program published beside it. Not a description of a program, and not the numbers a program once printed: the file itself, downloadable, on the page that quotes it. Most run in plain Node.js or the Python standard library with no dependencies and no licence to buy, which also means the next person to extend one does not need my permission or my machine.

Every check has been shown to fail on a deliberately broken copy of that program. A check that has never gone red is decorative — it is consistent with the code being right, and equally consistent with the check testing nothing. So each one is run against a mutated kernel first and has to reject it, and the count of falsifiers that fired is printed with the result.

Errors are recorded, with their date, in a public log — the errata — and never quietly fixed. Nearly all of the entries there were found by me, after publishing, which is the part that makes the log worth reading: a fabricated error floor that had to be retracted twice, and a modulus written into a kernel from memory as a prime that turned out to be composite, so a fingerprint check went on printing agreement while silently ceasing to be evidence. Neither was caught by a reader. The newest entry is dated 4 August 2026: source figures, correct as reported, shipped under the wrong method’s name on a live page and in its runnable pack — re-attributed three days after publication, again before any reader reported it.

None of that makes the work correct. It makes it checkable, which is a weaker property and a more useful one: you can disagree with a result here by running something, and the disagreement is then about the mathematics rather than about who is more credible.

Where the work has gone, and what has come back

Everything on this site is self-published and self-checked, so the honest question is what happens when it leaves. The complete record, with the status words meant exactly:

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.

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.

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 gate counts only once it has been shown to go red on a broken copy, a preregistration is committed before the instrument that tests it exists, and a hostile read precedes publication. The output rate is a consequence of that arrangement, and saying so seems better than letting a reader wonder.

These notes are self-published and not peer-reviewed. 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 Sage, in Magma, 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, carlos@carlostoledo.co, for everything: corrections, questions about a step, collaboration. There is no form — there is no backend behind one — and no queue: replies come from one person between other work and are often slow. A message that names the page and the one step it doubts can be answered properly; a general introduction usually cannot.

Some of this work is done for clients, mostly where a number that is quietly wrong is expensive to be wrong about, and enquiries are welcome at the same address.

site/about.html · rewritten 2026-08-03, revised 2026-08-04 · merged with the former contact page · no external fonts, scripts, stylesheets or images; the one script is same-origin, cookieless page counting · text CC‑BY 4.0