Why Closed Form exists
AI now writes research mathematics faster than people can read it. We translate it.
Each entry explains one result in plain words. It is not a summary. It tries to make you understand what the result says and why it was hard, starting from an example you can check yourself.
How we explain
Every explanation is one piece of continuous prose, not a form with fixed headings. It starts small: real numbers, a shape, or the simplest case where the claim already bites. Then it shows what people knew before and where they got stuck.
Next it names the one difficulty that made the problem hard, and says in ordinary words how the paper gets around it. We leave out the proof machinery. Any technical word is explained the first time it appears.
It ends with what the result does not say, and how far it has been checked. If we cannot make an idea clear without inventing something, we say so and stop.
Around every explanation. The facts stay separate and checkable: numbered sources, quotes matched word for word to the paper, a glossary, and a hype check.
Trust labels
Every result carries one label. It tells you how much checking stands behind the claim, not how important it is.
- Formal proof listed242 results →
At least one paper in the result is listed in the repository’s Lean catalogue, or its Lean notes link a Comparator challenge for a main result: a computer-checkable proof. A listing is not the same as an independent check.
- Partly formalized0 results →
The result links to Lean notes, but no listed proof or Comparator challenge for a main result.
- Claimed, not checked130 results →
Only the written paper exists. No computer has checked it, and it could contain errors.
What we don’t do
We don’t call a result true because a company published it. Many mathematicians have asked for careful review of AI results, and we agree.
On every entry. A hype check that says plainly how far the claim has been checked, and a direct link to the original paper.
How entries are made
- Draft. One AI model writes the explanation from the paper’s source and the published release. Every number in a worked example is computed, not guessed.
- Check. A different AI model matches every fact to a line in the paper and recomputes the examples. Anything it can’t match is cut.
- Correct. Anyone can report an error. Fixes are made in the open on GitHub.