LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models

Pavel Tikhonov; Elena Tutubalina; Ivan Oseledets; Dmitry I. Ignatov; Mikhail Seleznyov

cs.CLSep 26, 2026

LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models

Authors: Pavel Tikhonov, Elena Tutubalina, Ivan Oseledets, Dmitry I. Ignatov, Mikhail Seleznyov

Abstract

Language models can now prove theorems, but people still decide which problems to pursue. We ask whether a model's internal representations can help identify promising mathematical connections. We develop LANTERN, a fast, cost-efficient pipeline that uses a classifier over pretrained-model activations to rank candidate relations, followed by staged filtering, hypothesis generation, executable verification, and analytical checking. Applied to the On-Line Encyclopedia of Integer Sequences (OEIS), LANTERN ranked 50 million pairs among 10,000 frequently referenced sequences and produced 62 verified relations between pairs without an existing OEIS cross-reference. A content screen retained 13 relations worth presenting; nine of these are informative or insightful, including four which are entirely novel to the best of our knowledge: none appears in the OEIS or in our targeted literature search. The entire end-to-end process including classifier training, candidate ranking, filtering and verification took under 8 hours.

Figures & tables

Figure 1: Overview of Lantern . A classifier over pretrained LLM representations guides the search for relations between OEIS entries with no existing cross-reference. We found and verified 62 such relations; 13 of them are non-trivial, and for four of these we found no prior statement in the literature.

Figure 2: Composition of the 32 263 cross-referenced pairs in the corpus, text twins and the test pairs excluded. Only gold and silver, 9% of them, are used as positives; trivia, bare cross-references and random unlinked pairs are the negatives.

Figure 3: The split by date. The classifier is trained on cross-references present at

S_{0}

(2025-04-30, one day after the embedding model’s release) and tested on links people added afterwards: 927 pairs (265 with no word shared between the definitions) and 89 more added in 2026. Of these, 74 were selected by a frontier model as substantive relations.

Figure 4: The link classifier, drawn for Qwen3-32B. Each definition is embedded once into 65 layer vectors. A pair is described by the centred cosine between the two vectors at every layer and, at two layers (highlighted), by the element-wise product and absolute difference of the PCA-reduced vectors, as defined in Sec. 4.2 ; a logistic regression maps these features to a score.

Stage	Pairs remaining	From previous stage
Ranked queue	500	—
Cheap filter	118	23.6%
Hypothesis proposal	44	37.3%
Technical verification	44	100%

Table 1: The staged selection process for main-configuration run before the content audit. The queue contains the first 500 eligible pairs in the classifier ranking; the final stage requires both agreement with every stored term and an analytical derivation.

	S0 routine	S1 informative	S2 insightful	Total
N0 documented	22	0	0	22
N1 known elsewhere	2	3	2	7
N2 not found in search	0	4	2	6
Novelty not assessed	27	0	0	27
Total	51	7	4	62

Table 2: Cross-tabulation of novelty and significance for all 62 technically verified relations, before the content screen. S0 – S2 measure what the connection contributes; N0 – N2 measure what was already documented. N2 means not found by the OEIS and targeted literature searches, not established priority. Of the six N2 relations, four pass the screen: two S1 and two S2 .

Objects	Connection in plain language	Exact relation
1D and 2D cellular automata A071053 $\times$ A160239	N2 / S2 bridge. The live-cell counts of a planar automaton are recovered from the block factors of a one-dimensional rule (Sec. 5.2.1 ).	$g(k)=f(k)^{2}-f(k-2)^{2}$ ; $A(n)=\prod_{i}f(k_{i})$ , $B(n)=\prod_{i}g(k_{i})$ , where $k_{i}$ are binary run lengths.
Continued fraction and theta quotient A007325 $\times$ A227216	N2 / S2 bridge. Two analytic expressions combine to count a family of integer partitions, drawn as cell diagrams (Sec. 5.2.2 ).	$T(q)^{2}R(q)^{5}=\sum_{n\geq 0}c_{5}(n)q^{n}$ , where $c_{5}(n)$ counts 5-core partitions of $n$ .
Greedy sequence and Conway’s permutation A003278 $\times$ A006368	A sequence built by greedily avoiding three-term arithmetic progressions can instead be generated recursively through Conway’s permutation $B$ .	$c(0)=0$ , $c(2m)=B(2c(m))$ , $c(2m+1)=B(4c(m)+1)$ ; $S(n)=c(n-1)+1$ .
Pascal matrix and a change of basis A132440 $\times$ A039755	A change of basis turns the square of the dense lower-triangular Pascal matrix $P$ into a matrix with just two nonzero diagonals.	$M^{-1}P^{2}M=I+2T$ , where $M$ is the B-Stirling array and $T=\log P$ has only its first subdiagonal nonzero.
Partitions and necklaces A066633 $\times$ A185651	Deconvolving the counts $P(n,k)$ of parts of size $k$ in partitions of $n$ reveals divisibility. This recovers the totients used to count necklaces.	$\sum_{i=1}^{n}e(n-i)P(i,k)=[k\mid n]$ , where $e(m)=[q^{m}]\prod_{j\geq 1}(1-q^{j})$ .
Planar maps and a Catalan triangle A039598 $\times$ A000139	Ternary trees connect non-separable planar-map counts $M_{n}$ to a Catalan triangle $Q$ . This recovers a classical connection missing from the OEIS.	$T_{3}(x)=\sum_{n\geq 0}\frac{n+1}{2}M_{n}x^{n}$ , $C(x)=T_{3}(x/C(x))$ , $Q(n,k)=[x^{n-k}]C(x)^{2k+2}$ .

Table 3: Selected highlights from the 13 screened relations. All six pairs lack an OEIS cross-reference; the first two are the N2 / S2 connections explained in Sec. 5.2 . The examples span the N / S matrix in Table 2 and were selected for interpretability. Full statements and derivations, including the 62 technically verified outputs, are in Appendices A and F .

Figure 5: A 1D rule predicts 2D population counts. (a) The space–time diagram of Rule 150, one row per time step;

A(n)

counts the active cells in row

n

, and

f(k)=A(2^{k}-1)

is the count when

n

is a single run of

k

ones in binary. (b) The eight-neighbor Fredkin replicator, grown from a single active cell, at

n=1,3,7

; its single-run counts

g(k)=B(2^{k}-1)

are differences of squares of the 1D counts. (c) For any

n

, the lengths of the runs of ones in its binary expansion select the factors to multiply. At

n=13=(1101)_{2}

, runs of length two and one give

B(13)=g(2)\,g(1)=24\times 8=192

. Colors distinguish the two automata; filled cells are active.

Figure 6: From analytic expressions to finite diagrams. The continued fraction

R

and theta quotient

T

combine as

T^{2}R^{5}

to give the generating function of 5-core partitions. The coefficient of

q^{5}

is two: the diagrams shown are exactly the two qualifying partitions of five. Numbers inside cells are hook lengths, counting the cell itself plus those to its right and below; none is divisible by five.

Figure 7: Cross-references added after

S_{0}

: ROC-AUC of the surface-text scorer and of the classifier on three model sizes, all trained on the same labels, against unlinked pairs whose entries carry the same two topics as the linked pair (Sec. 6.1 ); the 42 substantive pairs and the 793 links with a matched background; whiskers are

\pm

1 SE. Qwen3.5-27B was released after

S_{0}

and may have seen the 42 pairs.

Appendix figures & tables6 assets

Supplementary material from the paper’s appendix.

Appendix

No.	Pair	N / S	Decision	Reason
1	A230877 $\times$ A334302	N2 / S1	excluded	The ordering is the definition of A334302; the substantive statistic is a relation to the A125106 encoding.
2	A053120 $\times$ A060187	N2 / S1	excluded	Chebyshev coefficients only produce the odd powers used in the recorded formula for A060187.
3	A103438 $\times$ A001498	N1 / S1	retained	Specific route through central factorial numbers and the Bessel coefficients.
4	A124733 $\times$ A266213	N2 / S1	retained	Specific Riordan-array composition and closed-form identity.
5	A000127 $\times$ A076839	—/ S0	excluded	Any two period-five sequences can be matched by a five-value table.
6	A132440 $\times$ A039755	N2 / S1	retained	Specific conjugation identity in the exponential Riordan group.

Appendix

Table 4: Screening ledger for the 62 statements listed below. The screen retains 13 relations that give a useful exact route or interpretation for a reader; nine are S1 or S2 . The remaining 49 are primarily definitional, representational, generic, or mechanically reproducible.

	gold	silver	trivia	bare cross-refs
graded by the screener (10 987 pairs)	369	2 436	8 182	—
used for training (10 770 pairs)	358	2 422	7 990	21 493

Appendix

Table 5: Graded cross-references in the corpus. The screener graded every pair whose formula or comments lines name the partner in

S_{0}

; the training set differs by the gold verdicts downgraded on re-reading and by the exclusion of text twins and of the test pairs of Sec. 3.2 . Bare cross-references name the partner only in crossrefs and were not graded.

scorer	percentile of the 74 pairs		74 pairs in	most-referenced in
	random	matched	top-1000	top-1000
surface text, untrained cosine (char TF-IDF)	63.5	59.0	2	1.8%
surface text, trained: LSA + logistic (Sec. 6.1 )	—	83.0	—	—
surface text, trained: LSA + boosting	—	90.5	—	—
raw cosine, one layer, untrained	70.3	66.3	1	1.7%
linear classifier (used)	77.3	77.4	1	6.3%

Appendix

Table 6: Scorers trained on the same 321 activation features (surface text excepted, trained on the same labels), tested on the 74 substantive future pairs (Sec. 3.2 ) against 500 000 random pairs and against popularity-matched peers (100 per pair for the text rows, as in Sec. 6.3 ); the column “most-referenced” counts pairs with an entry mentioned by at least 400 others (2.9% of random pairs). Averages favour boosting; the linear classifier puts the fewest most-referenced pairs in its top 1 000 (Sec. 4.2 ). The extreme top is fragile: two probes differing only in which layers feed the PCA block share one pair in their top-100 while their scores correlate at 0.5 over 500 000 random pairs.

	variant 1	variant 2	main
entries	5 000	5 000	10 000
positives	all links	gold, silver	gold, silver
	15 000	1 330	2 780
negatives	random	trivia, bare,	trivia, bare,
		random	random
one pair per entry	no	yes	yes

Appendix

Table 7: The three search configurations. Labels are those of Sec. 3.2 ; bare stands for pairs named only in CROSSREFS. The main configuration adds the caps of Sec. 4.2 and is the one tested in Sec. 6 .

stage	time
labelling of linked pairs (Claude Sonnet 5)	$\sim$ 2 h 40 min
Qwen3-32B activations, 10 000 entries	$\sim$ 1 h 20 min
classifier training, scoring of 50 million pairs	8 min
ranked queue of 500 pairs	20 s
filter (Claude Sonnet 5, no tools), 584 pairs	43 min
agent (Claude Opus 5 with tools), 118 pairs	2 h 56 min

Appendix

Table 8: Wall-clock time of each stage of the main configuration. Labelling (Sec. 3.2 ) ran in two parts, about 40 minutes for the popular entries and about two hours for pairs with a lesser-known entry. The filter reads the 500 queued pairs and 84 calibration pairs in batches of ten with four workers. The agent runs six pairs in parallel, with a median of seven minutes per pair; its time includes sandbox verification.

#	pair	class	novelty
1	A230877 $\times$ A334302	substantive	T1
2	A053120 $\times$ A060187	substantive	T1
3	A103438 $\times$ A001498	substantive	T1
4	A124733 $\times$ A266213	substantive	T1
5	A000127 $\times$ A076839	structural	T1
6	A132440 $\times$ A039755	mechanical	T1

Appendix

Table 16

Explore similar work

Aug 12, 2026

OEIS Open: How many conjectures can language models turn into theorems?

We construct OEIS Open, a benchmark based on 492 open mathematical conjectures from the OEIS, formalized in Lean by Tsoukalas et al. Whereas these conjectures had previously been attempted only with a bespoke agent, our open-source evaluation code runs any generic language model (LM) against them, and is secure against LM cheating attempts. We find that LMs equipped with a minimal set of tools resolve 147 of these conjectures with a budget of $50 per attempt, scoring 30% on OEIS Open. OEIS Open Lite is a random subset of 100 conjectures for cheaper evaluation. When evaluated with a budget of $200 per attempt, the best current LM scores 44% on OEIS Open Lite. Giving LMs access to the mathematics literature via 476,000 papers from arXiv did not increase performance on OEIS Open Lite, and nor did using more sophisticated agent loops. The conjectures covered in this work are of uncertain mathematical significance, and most have likely received little previous attention. Nevertheless, our results show that LMs can resolve open research conjectures autonomously and at modest cost.

Tom Adamczewski

Epoch AI

LLM Evaluation Automated Theorem Proving Mathematical Reasoning

Ask PDF

Sep 23, 2026

Learning to Discover Interesting Mathematics

Recently, Large Language Models (LLMs) have been increasingly able to solve advanced mathematical problems, including many that have been open for decades. This opens the door to expansion of mathematical knowledge at unprecedented scale. Yet, while LLMs may be able to conjecture and prove more and more theorems, it remains open whether this new mathematical knowledge is interesting or useful. We define intrinsic interestingness of a theorem as the ratio between the length of its proof and the length of its statement. We show that this correlates strongly with an extrinsic measure of the downstream utility of a theorem. We identify the difficulty of a proof conditioned on a set of premises as a useful primitive for computing these metrics, and train a 27B model that predicts proof difficulty more accurately than frontier general-purpose models. Optimizing for our metric creates a model capable of producing more interesting theorems, while also reducing substantial or full overlap with Mathlib from 91.9% to 30.6%, showcasing the creation of more out-of-distribution math. We show that our system can generate candidate theorems, select the most interesting among them, and iteratively build on a self-expanding mathematical library. These metrics provide a practical and quantifiable signal for ranking conjectures and guiding proof search within formal mathematical libraries. Our framework provides a path towards self-expanding, machine-verified mathematical libraries that can choose worthwhile statements without relying on human-supplied targets.

Niket Patel, Ahmad Rammal, Amaury Hayat +2

New York University · CERMICS, ENPC, Institut Polytechnique de Paris

Automated Theorem Proving Lean Theorem Proving Large Language Model-Guided Scientific Discovery

Ask PDF

Feb 27, 2026

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15

\%

accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.

Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat

1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study

Mathematical Reasoning Benchmarks Automated Theorem Proving LLM Mathematical Reasoning

Ask PDF