LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models

LANTERN. Illuminating Hidden Mathematical Knowledge in Language Models. By Pavel Tikhonov and four others. Published on the twenty-sixth of September. No code repository is linked to it.

Language models can now prove theorems. Choosing which problems are worth the effort is still left to people. This work asks whether a model's internal representations could help with that earlier step, by pointing at promising mathematical connections. If a model has absorbed relations it has never been asked to state, its activations might be a place to find them.

LANTERN is a fast, cost-efficient pipeline built on that hope. A classifier reads the activations of a pretrained model and uses them to rank candidate relations, so that the model's hidden knowledge decides where to look first.

After the ranking come stages of narrowing. Staged filtering, then hypothesis generation, then executable verification, then analytical checking. The target was the On-Line Encyclopedia of Integer Sequences, the OEIS. LANTERN ranked fifty million pairs drawn from ten thousand frequently referenced sequences. A ranking at that scale is only useful if the later stages can cut it down to a handful of claims that hold.

Out of that came sixty-two verified relations between pairs with no existing OEIS cross-reference. A content screen judged thirteen of them fit to present. Nine of those are informative or insightful, and four are entirely novel to the authors' knowledge: none appears in the OEIS or in their targeted literature search. The whole process, from training the classifier through ranking, filtering and verification, took under eight hours.

Fifty million candidates in, four new relations out, in less than a working day. Everything after the ranking narrows and verifies. The part this work hands to the model is the one people had kept for themselves: deciding which connections deserve a look at all.