Orientation — as of 2026-08-07T00:00:00Z
AI and mathematics right now, in plain words
If you arrived here because of a headline, this page is the place to start. It explains what is actually happening, what the technical words in the coverage do and do not guarantee, and where to look if you want to check something specific yourself. It takes about four minutes and assumes you know no mathematics.
From a generated proof to work others can use
Terence Tao's essay “Mathematics in the age of AI” describes a pipeline: generation, verification, clear communication, community digestion and acceptance, then canonicalization. Significance treats that as a set of separate questions rather than a single status label. A record can show the claim, the evidence, the parts a reader can explain, the people who have engaged with it, and whether later work has absorbed or reused it. Each entry keeps its author, date, source and scope, so progress at one stage is not mistaken for progress at another.
A layer an existing tracker can use
Significance is a reference implementation of an open record format, not a request that a problem site move its community elsewhere. An existing tracker can link to a record, copy selected fields into its own summary, or read the YAML directly. The standalone pages are a working demonstration; the useful outcome is a reviewer map and bounded open task that can travel back to the place where mathematicians already work.
What is actually happening
Large AI systems have started producing proofs of mathematical statements that no human had settled, and some of those proofs come with machine checkable files attached. That is genuinely new. What has not changed is how mathematics gets accepted: other mathematicians read an argument, work out whether it does what it says, and say so publicly under their own names. That process takes months and has barely started for most of the results being announced. Both things are ordinary at once — a real advance, and a settled question still open.
What a Lean certificate can guarantee
Lean is a program that checks formal proof terms. When its kernel accepts a proof term, that term establishes the formal statement relative to the axioms, toolchain and trust assumptions used for the check. This is a strong, precise guarantee about that formal object. A useful report must therefore name those assumptions and distinguish kernel checking from a build or another narrower automated check.
What it does not guarantee
Lean checks the statement it was given, not the statement in the paper. Somebody has to write the paper's theorem in Lean's language, and that translation is done by a person or a model and may not have been independently checked. If the translation quietly drops a hypothesis, weakens the conclusion, or proves a related-but-different statement, Lean will cheerfully accept it and report success. Reading the two statements side by side and confirming they say the same thing is a separate job, done by hand, and it is the job most often left undone. On this site that job has a name — correspondence — and where nobody has done it, the record says so.
What 'independently verified' should mean
The phrase gets used for at least three different things: that the authors ran their own checker, that somebody else re-ran it, and that a mathematician unconnected to the work read the argument and agreed with it. Only the third is what most readers hear. When you meet the phrase, the useful question is who did the checking, whether they were the same people who produced the result, and what exactly they checked — the file, the translation, or the mathematics.
What to ask when you see a claim
Four questions cover most of it. Which exact statement is being claimed? What was checked, by whom, and does the checker's name differ from the author's? What has nobody checked yet? And as of when — because a claim checked against a paper that has since been revised has been checked against something that no longer exists. Every record on this site is built to answer those four, and to say plainly where the answer is "nobody has".
What this site is, and is not
It records what was claimed, who said it, what evidence exists, and what remains open — with a name and a date against every line. It has no field for whether a claim is right, and it will not be growing one. If you want to know whether some result holds, this site cannot tell you; what it can tell you is exactly how much has been established so far, which is usually the thing people were really asking.
Where to go next
- The records — one page per claim, with evidence and open work.
- The ten results board — the same questions across every result at once.
- The glossary — every term above, one sentence each.
- Request or correct a record — one link is enough if the claim you care about is not here or a page needs changing.
What this page is not
- It is one editor's reading of the situation, dated and signed, not a neutral summary of the field.
- It says nothing about whether any particular result is right.
- It will go out of date. The date at the top is when it was last gone over.