Search

How this search works

At build time, every page on the site is rendered, stripped of its HTML tags, and written into a single JSON file alongside its title, description, category and date. When you open this page, your browser downloads that file once. Typing filters it locally.

The ranking is deliberately simple. A term appearing in a title is worth twelve points, in the description five, and in the body a value that grows with the logarithm of the number of occurrences and caps at six. Every term you type has to appear somewhere on a page for it to be returned, so adding words narrows results rather than widening them. Matches are highlighted in both the title and the snippet.

There is no stemming, no fuzzy matching and no synonym expansion. Searching for prove will not find proof. This is a real limitation and the fix is a stemmer, which would add a dependency and several hundred lines to search twenty-eight pages. If the archive grows past a few hundred articles it will be worth doing.

What is in the index

Every page the site publishes: every article, plus the home page, the archive, the solver and the four static pages. The static pages are indexed alongside the articles because people looking for the accessibility commitments or the reuse terms should find them by searching rather than by hunting through the footer.

For each page the index carries the URL, the title, the one-line description, the category, the publication date and the full body text with markup removed. Nothing else. There are no keywords, no hidden terms and no ranking adjustments applied by hand, so a page that appears at the top does so because the words you typed are in its title or occur repeatedly in its text.

The whole file is a little over two hundred kilobytes uncompressed, which arrives as considerably less over the wire because the server compresses it. That is the price of the entire archive being searchable offline once the page has loaded. Search again after you lose connectivity and it still works, because there is nothing left to fetch.

Getting better results

Terms narrow rather than widen, so start with one word and add a second only if the first returns too much. Searching for proof returns most of the archive. Searching for proof kernel returns the pieces that discuss what a proof assistant's trusted core actually does.

Search for the specific noun rather than the concept. The articles name things precisely, so Mathlib, shunting-yard, discriminant, tokeniser, discharging and DRAT all land on exactly one or two pages. General words like reasoning or intelligence appear everywhere and sort poorly.

Search for a person or a system if you remember one. Names carry well here: Strassen, Erdős, Ramanujan, Gonthier, Kempe, AlphaGeometry, AlphaTensor, Lean, GIMPS, Graffiti.

Because there is no stemming, try the other form if a word returns nothing. Singular and plural are different terms. So are formalise and formalisation. British spellings are used throughout, so colour finds the four colour theorem piece and color does not.

Highlighting shows you why a page matched. If the marked words are all in the snippet and none in the title, the match is probably incidental and the page below it may be the one you want.

Why not a hosted search service

Because a hosted search box sends every keystroke to a third party, along with your address and enough context to build a profile of what you were curious about. That is the standard arrangement and it is invisible to the person typing.

Doing it locally costs one file download of a few hundred kilobytes, which is less than a single photograph on most sites, and it means the query never leaves the browser. Open your network tab and watch: there is one request for the index when the page loads, and nothing after it, however much you type.

The same reasoning governs the rest of the site. No analytics, no cookies, no third-party scripts. The one thing that ever leaves your browser is a message you deliberately send through the contact form. The privacy page explains how to verify all of it in about a minute.

If search does not find it

The full archive listing shows every article with its category, description and date, ordered newest first, and that page also carries a short guide to reading the collection in a sensible order if you are starting cold.

The archive is also organised loosely into four groups. History covers results that machines settled and humans could not check, including the four colour theorem and the 200-terabyte proof of the Boolean Pythagorean triples problem. Mechanism explains how the systems work, including tokenisation, chain of thought and what a proof assistant kernel actually does. Analysis covers benchmark contamination and how to read a capability claim. Puzzles covers riddles and the boundaries of computation.

There is also a feed if you would rather be told when something new appears than come back and check. It is an Atom feed carrying the full text of every article, not a truncated summary that forces a click, and it works in any reader.

Known limits

Four, stated plainly rather than discovered by you.

No stemming or fuzzy matching, as described above. A misspelling returns nothing rather than a suggestion.

No phrase search. Quoting a phrase has no effect; the words are treated separately and a page containing all of them anywhere will match. For an archive this size that has not been a problem in practice, and adding it would mean storing positional data that roughly doubles the index.

Ranking is a fixed formula rather than anything learned from what people click, because nothing here records what people click. A term in a title outweighs a term repeated twenty times in a body, which is usually right and occasionally buries a page that discusses your topic at length under one that mentions it in a heading.

Search requires JavaScript, since the filtering runs in your browser. With scripts disabled this page shows the input and the explanation and nothing happens when you type. The archive listing is the fallback and it needs no scripts at all.