Machines that do mathematics, examined honestly.

There are two comfortable positions on artificial intelligence and mathematics, and both are wrong in ways that are easy to demonstrate.

The first is that the problem is essentially solved. Systems score gold medals at the International Mathematical Olympiad, they pass benchmarks that stumped researchers three years ago, and the remaining gap is a matter of scale. This position survives only if you do not look at how the benchmark numbers were produced, or at what happens when a famous problem is altered so the famous answer no longer applies.

The second is that none of it counts, because a statistical model predicting tokens cannot understand anything and therefore cannot do mathematics. This position has to explain away a growing list of specific results: a matrix multiplication algorithm that improved on a bound standing since 1969, a knot theory relationship found by a neural network and then proven by humans, competition problems solved by a system that invents the auxiliary construction and hands the deduction to a symbolic engine.

Neither camp is being careless on purpose. They are looking at different evidence and neither is checking the other's. This site tries to hold both sets of evidence at once, which mostly means being specific about which component of a system produced which guarantee.

That framing recurs across almost every article here, because it turns out to be the load-bearing distinction. Modern mathematical AI is not one thing. It is a neural component that proposes and a symbolic component that verifies. AlphaGeometry pairs a language model with a deduction engine. AlphaProof pairs one with the Lean type checker. A SAT solver pairs learned branching heuristics with a resolution proof that a formally verified checker reads line by line. In every case the creativity comes from the part that can be wrong, and the certainty comes from the part that cannot.

Once you have that lens, a lot of confused argument resolves. A model that produces an unverified proof has produced a conjecture. A model that produces a Lean term which type-checks has produced a theorem. These are different objects and the difference has nothing to do with how convincing the prose was.

The articles fall into a few groups. Some are history: the four colour theorem and the first proof no human could read, seventy years of trying to teach machines arithmetic, thirty years of volunteers hunting Mersenne primes. Some are mechanism: what chain of thought actually buys you, why tokenisation makes counting letters hard, what a proof assistant kernel does. Some are honest accounting: the benchmark contamination problem, how to check a derivation you did not produce, what olympiad performance does and does not indicate. And some are puzzles, because a riddle with a changed premise is the cheapest diagnostic anyone has for telling memorisation from reasoning.

Everything here is written for a reader who is comfortable with secondary-school mathematics and willing to follow an argument. No prior knowledge of machine learning is assumed. Where a claim rests on a specific paper or result, the paper is named, so you can go and disagree with it directly rather than with a summary.

A recurring theme worth flagging in advance, because it runs through more than half the archive: the gap between knowing a thing is true and understanding why it is true keeps widening. The four colour theorem was settled in 1976 by checking 1,936 configurations, and nobody can point at the argument and explain what makes the number four. The Boolean Pythagorean triples problem was settled in 2016 with a 200-terabyte proof log, and nobody knows what changes at 7,825. Both results are certain. Neither is illuminating. As more mathematics gets settled by search rather than by insight, that gap is the cost, and no one has proposed a way to close it.

The counterweight is formalisation. A proof checked by a small kernel against explicit axioms is trustworthy in a way that a ninety-page paper read by two referees is not, and Mathlib now contains enough mathematics that formalising a new result costs about as much as writing it up informally. That shift is quieter than the olympiad headlines and it will probably matter more.

We publish irregularly, we take corrections seriously, and we would rather post nothing than post a number we have not checked.