Scientific knowledge can be public yet remain undiscovered, buried under the sheer volume of new research. Henri Poincaré, who died in 1912, is often called the last person to know all the major mathematics of his era. A century later, a Canadian survey found nearly a third of mathematicians couldn’t keep up with relevant research and scholarly news. Among early-career researchers, the figure hit 43%. Senior scientists fared better, the study notes, because they had built networks of friends and colleagues. When Google failed, they knew whom to ask.

In the era of large language models, young researchers have also gained a valuable acquaintance. But even a capable AI assistant has its limits. Say a mathematician wants to know whether a theorem already exists. They type a query, press Enter, and Google Scholar returns 30 papers with matching keywords. Now someone, human or agent, has to read through thousands of pages for a chance of finding that one statement. A waste of time, effort and tokens? That’s exactly what the people behind theoremsearch.com thought when they set out to properly index all of research mathematics.

LLMs take too long to respond and “hallucinate like hell” when reading long PDFs, senior author Vasily Ilin told Nebius Science. Even with a specific source in hand, a simple “does this theorem exist” question becomes, in his words, “a nightmare”. There’s always old-fashioned Command+F, of course. But you rarely know the exact wording the authors used, and the tool handles math notation poorly. In many cases, finding a paper is not enough — math needs a finer grain, indexed at the level of individual theoremes. Only then you can quickly check whether a given statement already exists. That’s the goal the eight members of the University of Washington Math AI Lab, which Ilin directs, have set out to accomplish.

Consider two statements: “My body and mind currently have little power” and “I do not feel like doing anything now.” They share not a single word, yet both mean “I am tired.” The same happens in mathematics — logically equivalent statements can take wildly different forms. So how do you build meaningful search over a large corpus? One approach is to let a language model play with different wordings of the same idea while running simple string searches. It’s as slow as it is costly.

The solution is embeddings: map each statement to a vector such that semantic similarity becomes geometric proximity. Two sentences that share no vocabulary but express the same idea should land close together in the embedding space. As an example, here’s how Qwen3 8B Embedding ranks four phrases by similarity to “I am tired ‘:

“I do not feel like doing anything now” scores at 0.73,

“My body and mind currently have little power” at 0.72,

“My heart is about to stop” — 0.66,

“Dinosaurs aren’t real” — 0.49.

It works! Turning this into a search engine is straightforward: embed the query, find its nearest neighbors in the embedding space, and return the corresponding statements. So Ilin’s team did something that “wasn’t done just because nobody did it ‘: they scraped around 600,000 mathematical papers, parsed over 9 million statements from them (theorems, lemmas, propositions) and embedded the entire corpus with Qwen3. Essentially every theorem in research mathematics was now indexed by its meaning.

But when they ran test queries against the new index, the results were terrible. Qwen3, like every major embedding model, was trained on natural language, and that is not how mathematics is written. Take a standard theorem from complex analysis:

\oint_\gamma f (z), dz = 2\pi i \sum_{k=1}^{n} \operatorname{I}(\gamma, a_k),\operatorname{Res}(f, a_k).

Just as it is ugly to anyone outside mathematics, heavy symbolic notation is opaque to an embedding model: the tokens carry little meaning in natural language. That might soon change, with newer models being very capable of processing mathematical text. However, for now the UW Math AI Lab turned to what Ilin calls their ''single main innovation'' — using an LLM to restate every theorem in plain English.

The Theorem Search authors call these representations slogans. Here is the slogan for the residue theorem above: “The integral of the function around the closed curve equals two pi i times the sum, over all the singular points, of the winding number of the curve about each point multiplied by the residue of the function there .” How much does this help? Take an equivalent natural language formulation as the query: “A closed contour integral of the function evaluates to the poles' residues, each scaled by the contour’s winding number about that pole, with the aggregate multiplied by two pi i.” Qwen3 scores the slogan at 0.88 against it, while the symbolic original manages only 0.81.

Both equivalents score well, but across 9 million theorems the seemingly small gap compounds into a twofold difference in performance. The metric is Hit@20, which asks a simple question: how often does the statement the mathematician wanted appear in the first twenty results? To build the test, three research mathematicians wrote 111 queries blind, describing theorems they knew existed without ever looking at the Theorem Search corpus or its slogans, so none of the system’s own phrasing could leak into the questions. On this test, indexing by slogans pays off twice over.

Embedding the raw symbolic notation with Gemma lands a Hit@20 of just 0.09: the right theorem makes the top twenty only nine percent of the time. Feed the same model the plain English slogans instead and the figure jumps to 0.25. The best configuration, the familiar Qwen3 8B embedder, reaches 0.45, putting the correct statement in the shortlist nearly half the time.

Mathematicians looking for theorems they already know exist tested the service’s assistance in remembering rather than in genuine rediscovery, and Hit@20 of 0.45 might not sound astonishing — until you compare it with the tools scientists actually use. Filtered Google search tops out at 0.38 and can only ever point you to a paper, never a theorem. arXiv’s own search found the right paper in just two of the 111 queries.

Frontier models fare little better: ChatGPT-5.2 scores 0.2, Gemini 3 Pro 0.27. The specialised index beats general-purpose search by a wide margin, and unlike the rest it hands the mathematician the single lemma buried on some paper’s fortieth page rather than the whole document to read.

The team has also found several ways to push the tool’s quality further. Theorems often lean on notation defined pages earlier, leaving a language model without the context to write a proper slogan. As Ilin puts it, “In a theorem you’ve got, say, a capital H. And what is this H?” On a controlled slice of the corpus, slogans written from the bare statement put the right result in the top ten 66% of the time; let the LLM read the paper’s opening section first, and Hit@10 climbs to 0.74.

The second booster is a second pass: after pulling a hundred candidates by rough likeness, a smaller but more diligent model weighs each one against the query and re-sorts the list. The third improvement is the easiest of all: a better model writes better slogans. Theorem Search mostly relied on the open-source DeepSeek; swapping it for Claude Opus 4.5 lifts top-twenty accuracy from 0.74 to 0.84.

4,000 USD in API costs for slogan generation and 2,000 USD for cloud compute and storage, sponsored by Nebius Token Factory: that was the humble price of gathering all of research mathematics into a single searchable corpus. Unfortunately, 85% arXiv articles are licensed to not be redistributed, so the publicly available dataset is a limited volume of around 1.5 million theorems. The database is easy to maintain and cheap to extend with new papers, whether weekly, daily or hourly. Theorem Search also exposes a REST API and an MCP server, offering itself to AI agents, which may well become its most prominent users and solve the rediscovery problem for mathematics.

The question “has this already been established” barely scratches the surface of knowledge retrieval problems. Consider, for example, another one — just as simple to pose and yet even harder to answer: which other theorems a given result depends on? What one would ultimately like to have is not only an index of mathematics but an entire dependency graph.

Millions of statements all united in a single network with all of the possible links established. Some people have been building toward that future for a while now, maintaining the libraries of so-called formalized mathematics that make proof-assistants like Lean possible. But the pace of the research progress inevitably leaves any number of passionate bookkeepers behind. If only it was possible to somehow automate the process of mathematics formalization — that is the big project of the UW Math AI Lab, Theorem Search being the first necessary step.”