Mathematicians have always evaluated proofs on more than just whether or not they are correct.
Some proofs are memorable because they introduce an elegant idea. Others matter because they reveal a new way to approach a problem. Some stand out because they solve familiar questions using methods that were difficult to anticipate.
Correctness has been mechanically verifiable for decades, while novelty has always been much harder to evaluate. There has never been a reliable way to measure how surprising a proof was based on the mathematical knowledge available when it was created.
PriorProof, Neel Somani’s research project on measuring mathematical novelty, explores one possible solution: treating time as part of the measurement.
As automated theorem provers begin producing formal mathematics at increasing scale, determining which proofs represent meaningful advances may become nearly as important as verifying that they are correct.
Why Formal Proofs Create a Path to Measuring Novelty
The hardest part of measuring novelty is identifying what a proof actually assesses.
With traditional mathematical writing, that is often a matter of interpretation. Two mathematicians can look at the same proof and disagree about which techniques it uses, which earlier ideas it builds upon, or whether its approach is genuinely unusual.
That makes objective measurement difficult. A novelty metric that depends on human judgment risks reproducing the same uncertainty it is trying to eliminate.
Somani’s approach begins with formal mathematics.
In the Lean proof assistant and its community library, Mathlib, proofs are converted into precise formal objects whose dependencies can be examined mechanically. The library’s commit history also records when each theorem was introduced.
That creates two pieces of information that are difficult to obtain from traditional mathematical writing: the ingredients used in a proof and the state of mathematical knowledge available at the time.
The system does not require human annotations, manually defined categories of proof techniques, or a language model deciding what a proof “really” does.
Comparing New Proofs Against the Mathematics of Their Time
The core idea behind PriorProof is simple: a proof is more novel when it uses techniques that would not have been expected when it was created.
For a theorem proved at a particular point in time, the system first extracts its dependency footprint — the mathematical tools and results that the proof ultimately relies on.
Helper lemmas created within the proof are expanded recursively into the earlier results they depend on. Routine implementation details are removed so the footprint represents mathematical ideas rather than technical bookkeeping. Related dependencies are also grouped into broader families so that an obscure function name is not mistaken for a genuinely new technique.
The next question is historical: given what was known at that moment, what would a mathematician have expected this proof to use?
To answer that, PriorProof builds a historical prior using only the version of Mathlib that existed before the proof was created. It finds earlier theorems with similar statements, examines their statements rather than their proofs, and looks at the mathematical tools those earlier proofs relied on.
A proof that follows an expected path receives a lower novelty score. A proof that uses ingredients outside the patterns established by earlier work receives a higher score.
A key part of the framework is that novelty depends on time.
Many influential proofs appear less surprising in hindsight because their techniques later become standard. PriorProof evaluates each proof against the mathematical landscape that existed when it was first introduced, rather than against what researchers know today.
How PriorProof Avoids Looking Back With Future Knowledge
One of the most important design choices in PriorProof is avoiding hindsight.
Any historical measurement faces the risk that future information will accidentally influence the evaluation of past events. Somani addresses much of that problem by building the historical prior from a snapshot of Mathlib taken before the proof was created.
That prevents later mathematical developments from affecting earlier measurements.
The project also identifies two remaining sources of potential leakage: pretrained models used during retrieval and the model used to encode theorem statements. Rather than assuming those risks do not exist, the framework includes tests designed to determine whether results change when historical information is replaced with unrelated material.
The metric is also explicit about what it does not capture.
Some mathematical breakthroughs are important because they introduce entirely new definitions. Others create unexpected connections between different areas of mathematics. PriorProof is not designed to measure every form of mathematical creativity, and those areas remain possible directions for future work.
The project also acknowledges a source of bias: mathematical ideas can spread through teaching, collaboration, and informal knowledge sharing without appearing in formal proof dependencies.
That means some genuinely novel proofs may appear less surprising than they actually were. In practice, the metric is more likely to underestimate novelty than overstate it.
Defining those limits is part of what makes the approach useful.
From Mathematical Proofs to AI-Generated Discovery
The motivation behind PriorProof comes from the rapid progress of automated theorem proving.
Language-model-based systems are increasingly capable of generating formal proofs at a pace that human researchers cannot easily review. Formal verification can determine whether those proofs are correct, but correctness alone does not identify which results introduce meaningful new ideas.
That is where a novelty measure could become useful.
A scalable system for ranking mathematical surprise could help researchers, journal editors, and formal library maintainers focus attention on proofs that represent genuine advances rather than variations of existing methods.
Somani’s roadmap also includes broader applications, including methods for comparing machine-generated proofs more fairly across different systems.
Before moving into machine learning research, Somani worked as a quantitative researcher covering financial markets. PriorProof reflects that background: define the concept precisely, avoid look-ahead bias, test assumptions, and evaluate results using measurable evidence.
His earlier GPT-Erdos project followed a similar philosophy, using Erdős problems as a way to study how language models generate and evaluate mathematical reasoning.
Whether PriorProof’s specific scoring method becomes the standard approach is not the central question.
The broader contribution is the idea that mathematical novelty, something usually treated as an intuitive judgment, can be studied as a measurable property.
As machines become more involved in mathematical discovery, distinguishing between proofs that are merely correct and proofs that genuinely advance the field may become just as important as verifying the proofs themselves.
Leave a Reply