Imagine a proof that says, in effect, “This follows from a result in that paper.” The cited paper may run dozens of pages. Somewhere inside it is the definition, lemma, or theorem the proof needs—but the citation points to the whole work, not the precise stepping-stone. For a reader trying to trace an argument, that can feel less like following a map than searching a library with the shelf labels missing.
A June 2026 paper by Simon Kurgan and colleagues tackles that problem by changing what a mathematical search system keeps track of. Instead of treating each paper as one item, their system, TheoremGraph, tries to build a map of individual mathematical statements and the relationships between them. The goal is not to prove new theorems. It is to make the existing landscape easier to navigate: find a result, see what it depends on, and connect it to a version written in a different mathematical language.
Building the first side of that map means mining ordinary research papers. The team’s parser identified more than 11.7 million theorem-like statements in mathematics papers on arXiv and proposed 18.3 million directed links between them. Some links are straightforward: a paper labels a statement as a theorem and explicitly refers to it elsewhere. Others are harder to spot. A proof may cite an earlier paper, mention a theorem in its prose, or use notation defined several pages earlier.
So the researchers combine several ways of finding connections. One follows explicit references. Another uses clues in nearby text and backward references in a paper. A third looks for notation introduced in one statement and used in another. Crucially, the proposed links carry labels showing which method found them. That lets a user distinguish a clear reference from a more speculative connection, rather than treating every edge in the map as equally reliable.
The difference matters. In a check of 500 papers, an independent language-model judge accepted 98.8% of the links from the explicit-reference method, but 76.6% of heuristic links and 42.7% of notation-based links. Across the combined set, the system’s measured F1 score was 0.642 against that judge. Those figures are not a final verdict on every connection: the judge itself is not mathematical ground truth, and the validation covered a sample. But they make the central point plain: a large graph of candidate dependencies can be useful only if its uncertainty stays visible.
The second side of the map comes from Lean, a proof assistant in which mathematical statements and proofs are written in a formal language that a computer can check. In a formal proof, dependencies are spelled out in much finer detail than they usually are in a research paper. The team built LeanGraph to extract them from 25 Lean projects, producing 388,105 declaration nodes and more than 11.3 million typed edges. Those edges distinguish, for example, a result used in a theorem’s proof from a definition needed to state it.
But the two maps speak different dialects. A paper describes a theorem in prose and conventional notation; Lean records it in a precise formal syntax. To connect them, the researchers turn each statement into a short natural-language description, or “slogan,” then place those descriptions in a shared semantic space. Statements that mean similar things should land near one another, even if they share few exact words. A language-model judge then checks proposed matches, separating exact matches from looser relationships and false look-alikes.
The system proposed 100,799 formal-to-informal matches above its chosen similarity threshold. The judge accepted 47,952 as matches. At the highest similarity tier, at least 0.9, it accepted 87% of candidates. A separate check used human-written blueprints that already pair Lean declarations with informal statements: the system retrieved the annotated partner first 43.5% of the time and within its top ten results 69.9% of the time. Some apparent misses were useful alternatives—another statement expressing a closely related result—while others were genuine mismatches. Similarity is a way to find candidates, not a substitute for checking their hypotheses.
Could this map help with the practical task of locating a formal result from an informal query? On one benchmark of 810 queries, a configuration combining statement names, signatures, search adjustments, and graph structure reached a Recall@10 score of 0.775. That means the target appeared among the first ten results for roughly three quarters of the queries. A competing system with a reranker scored 0.780; the researchers report that the scores were close, not that the methods were proven equivalent. Their test on another task also warns against overgeneralizing: techniques that helped locate a mathematical concept performed worse when the goal was to retrieve the particular lemmas used in a proof.
That distinction points to the larger challenge. Finding a theorem that says roughly the right thing is not the same as finding the exact result a proof needs. A special case can look like a general theorem; similar notation can conceal different assumptions. TheoremGraph’s contribution is a method for organizing and connecting evidence across two very different kinds of mathematical record—not an automated certificate that every link is correct.
If the approach matures, it could make mathematical literature feel less like a stack of isolated papers and more like a network of arguments: claims linked to earlier claims, formal proofs linked to their human-readable counterparts, and uncertain connections marked for inspection. The map will not tell mathematicians which route is right. It may help them find the relevant paths—and notice when a familiar-looking road leads somewhere else.
