The "First Proof" Experiment

A group of mathematicians—including Martin Hairer, Daniel Spielman, and others—has released a provocative benchmark titled First Proof. Unlike standard AI benchmarks which rely on competition problems (IMO, AIME) or synthetic datasets, this paper presents ten private research-level questions that arose naturally in the authors' own work.

The twist? The answers are known to the authors but have never been published. They are currently hosted in an encrypted format on the project website, with the decryption key scheduled for release on February 13, 2026.

Terence Tao noted that this structure revives the Renaissance tradition of "challenges," where mathematicians would send encrypted announcements of their discoveries (anagrams) to claim priority before revealing the proof.

Mining the Erdős Problems

A massive collaboration led by Google DeepMind and researchers at Caltech has applied Gemini to the Erdős Problems—a database of conjectures posed by Paul Erdős.

The team focused on 700 conjectures labeled "Open." Their agent, Aletheia, utilized a hybrid approach:

1. Generation: The model generated candidate proofs or counterexamples.
2. Verification: A separate "verifier" routine filtered these candidates.
3. Expert Review: Human mathematicians evaluated the surviving candidates.

The results were mixed but illuminating. The system successfully addressed 13 problems. However, the breakdown reveals a subtle nuance in "AI discovery":

• 5 problems were solved with seemingly novel autonomous solutions.
• 8 problems were technically "solved" by the AI, but only because the AI successfully identified that the problem had already been solved in obscure literature.

This highlights a new risk: Subconscious Plagiarism. The models occasionally reproduce arguments they have seen in their vast training corpus without attribution, presenting them as original derivations. The paper suggests that for many "open" problems, the difficulty lies not in the mathematics, but in the obscurity of the existing literature.

Rethinking R&D: The Bell Labs Architecture

Based on "How technoscientific knowledge advances: A Bell-Labs-inspired architecture" by Venkatesh Narayanamurti and Jeffrey Y. Tsao.

We often imagine innovation as a pipeline: basic science creates a discovery, applied research refines it, and development turns it into a product. This "Linear Model" is deeply embedded in how we fund and manage science. But according to Venkatesh Narayanamurti (former Dean of Harvard SEAS) and Jeffrey Tsao (Sandia National Labs), this model is fundamentally flawed—and it’s stifling modern discovery.

In their paper, they propose a different architecture for knowledge advancement, modeled after the 20th century’s most successful innovation engine: Bell Labs.

The Architecture: Bell’s "Dodecants"

Narayanamurti and Tsao argue that we must abandon the "Science vs. Technology" dichotomy. Instead, they model innovation as a 12-part grid—the Dodecants—formed by crossing Six Mechanisms of action with Two Flavors of intent.

The Six Mechanisms (The "Verbs")

The authors break down the "Scientific Method" ($\dot{S}$) and "Engineering Method" ($\dot{T}$) into three distinct steps each. These are the engines of the process:

• $\dot{S}_1$: Fact-Finding. The accumulation of new data and observations (e.g., measuring the spectral lines of hydrogen).
• $\dot{S}_2$: Explanation-Finding. Creating models or theories to make sense of facts (e.g., Bohr’s model of the atom).
• $\dot{S}_3$: Generalizing. Extending theories to cover broader classes of phenomena (e.g., Quantum Mechanics).
• $\dot{T}_1$: Function-Finding. Identifying a specific utility or need (e.g., "we need to amplify this weak signal").
• $\dot{T}_2$: Form-Finding. Designing the physical structure to achieve that function (e.g., the geometry of a transistor).
• $\dot{T}_3$: Exapting. Radical repurposing—using a technology for a completely unintended use (e.g., using a microwave radar magnetron to cook food).

The Two Flavors (The "Adverbs")

Crucially, any of the six mechanisms above can be performed with two different mindsets:

• Research Mode (R): Seeking Surprise. This is divergent thinking, aiming to disrupt current understanding or capability.
• Development Mode (D): Seeking Consolidation. This is convergent thinking, aiming to refine, stabilize, and make robust.

This creates the 12 "Dodecants." You can do "Explanation-Finding in Development Mode" (refining a known theory) or "Form-Finding in Research Mode" (trying a crazy new transistor design just to see if it switches).

The Problem: Broken Cycles

The magic of Bell Labs wasn't just having smart people; it was the fluid movement between these sectors. A physicist stuck on Explanation-Finding ($\dot{S}_2$) could walk down the hall to an engineer doing Form-Finding ($\dot{T}_2$) and realize that a manufacturing anomaly was actually a new quantum effect.

Modern R&D often breaks these cycles. "Science" grants fund only the $\dot{S}$ mechanisms, while corporate R&D funds only the $\dot{T}$ mechanisms (and usually only in "Development" mode). The Exapting ($\dot{T}_3$) mechanism—often the source of the biggest breakthroughs—is particularly starved because it fits neither pure theory nor immediate product roadmaps.

Conclusion

The decline in disruptive breakthroughs isn't due to a lack of ideas, but a rigid architecture that prevents the "Dodecants" from feeding each other. To revive the spirit of Bell Labs, we don't need more money poured into the same silos; we need to nurture the full cyclic flow between surprise and consolidation, facts and functions.

Taming Mathematical Complexity: How Software Engineering is Reshaping Pure Mathematics

Based on "Abstraction Boundaries and Spec Driven Development in Pure Mathematics" by Johan Commelin and Adam Topaz.

Modern mathematics has a scaling problem. New results are becoming increasingly intricate, often relying on deep mastery of multiple disparate subfields. Significant papers now routinely exceed one hundred pages, and the peer review process can drag on for years.

In a recent paper, Johan Commelin and Adam Topaz argue that the traditional methods of managing this complexity are hitting their limits. Their solution? Applying principles from software engineering—specifically Abstraction Boundaries and Spec Driven Development—within the rigid environment of Interactive Theorem Provers (ITPs) like Lean.

Here is how these concepts helped a distributed team of mathematicians resolve one of the most difficult challenges in modern arithmetic geometry: The Liquid Tensor Experiment.

The Problem: Inherent vs. Accidental Complexity

The authors distinguish between two types of difficulty in mathematics:

• Inherent Complexity: The raw difficulty of the ideas and the breadth of prerequisites required to understand a proof.
• Accidental Complexity: The friction caused by imperfections in communication—unwritten assumptions, ambiguous definitions, or the mental tax of tracking trivial side conditions (like ensuring a number remains positive throughout a proof).

While mathematicians have long used "abstraction" to simplify problems, the authors argue that doing this on paper often leaves room for accidental complexity to creep back in.

The Solution: Spec Driven Development (SDD)

Commelin and Topaz advocate for Spec Driven Development, a workflow where the "specification" (the external behavior of a mathematical object) is separated from its "implementation" (how it is constructed).

In a computerized proof assistant like Lean, this allows for a radical change in workflow: Mathematical Debt.

Using the keyword sorry, a user can create a placeholder for a proof or definition that doesn't exist yet. This allows researchers to write high-level proofs using objects that haven't been built. For example, a mathematician can prove a theorem about an "Abelian Category" by simply asserting that the category exists (tagged with sorry), allowing them to make progress on the main theorem without getting bogged down in the construction details immediately.

This recursive process involves:

• Isolating a target (definition or theorem).
• Writing a "Spec" (interface) for it.
• Breaking it down into smaller, lower-complexity parts.
• Repeating the process.

The Case Study: The Liquid Tensor Experiment (LTE)

The paper uses the Liquid Tensor Experiment as its primary example. Initiated by Fields Medalist Peter Scholze, the goal was to verify the main theorem of "Liquid Vector Spaces"—a result Scholze described as his most important to date, but one so complex he could no longer hold the entire argument in his head.

By using Spec Driven Development, the team could distribute the work among a dozen contributors. An expert in homological algebra could work on the Ext groups, while another contributor worked on the specific properties of p-Banach spaces, connected only by the rigorous "handshake" of the abstraction boundaries.

Crucially, this method allowed for refactoring. Just as in software, if a definition needed to be changed (e.g., how Ext groups were implemented), the ITP ensured that the change only affected local files, while the high-level logic remained valid as long as the external "spec" was satisfied.

The "Duck Test": Trusting the Code

A common critique of formalized math is the "Alignment Problem": How do we know the code actually represents the math we care about? What if the definition of a "manifold" in the computer is slightly wrong?

The authors propose using Abductive Reasoning (inference to the best explanation). They created a test suite of examples to verify their definitions. If the formalized object behaves like the mathematical object in all standard cases—if it looks like a duck and quacks like a duck—we can trust it is a duck.

Conclusion

Commelin and Topaz argue that while ITPs have a steep learning curve, they offer a way to "tame" the explosion of complexity in modern research. By enforcing strict abstraction boundaries, computers don't just check proofs; they allow mathematicians to collaborate at a scale that was previously impossible, turning the solitary act of proof-writing into a distributed, architectural engineering feat.

Notes on the structure of Mathlib: Part I

I analyze the structure of Mathlib—the mathematical library for Lean 4—as a network. By constructing a co-occurrence graph from 118,517 theorem proofs, I find that formalized mathematics is shallow (81% of premises lie within two hops of reflexivity), naturally modular (493 communities emerge that correspond to mathematical subfields), and contains structural anomalies (premises that are well-connected but underused). The predictive model I trained is largely tautological—degree alone accounts for 89% of its accuracy—but the anomalies it surfaces merit investigation.

The Question

Mathlib contains over 150,000 formalized theorems. How is this knowledge organized? What does the dependency structure reveal about mathematics itself?

I constructed a graph where nodes are premises (lemmas, definitions, theorems) and edges connect premises that co-occur in proofs. The data comes from LeanDojo Benchmark 4, which traces 118,517 theorem proofs. After filtering edges that appear fewer than 3 times, the graph contains 11,789 nodes and 82,567 edges.

Finding 1: Mathematics is Shallow

I computed the shortest-path distance from each premise to a set of "core" nodes: rfl, symm, trans, mul_comm, and mul_assoc. The distribution is striking:

Over 80% of premises lie within two hops of foundational axioms. The maximum depth is 7. Formalized mathematics, at the proof level, is shallow.

This does not contradict the intuition that advanced mathematics builds on long chains of abstraction. A theorem may logically depend on many prior results, yet its proof may "reach back" to rfl directly. The shallowness is structural, not logical.

Finding 2: The Core

PageRank identifies the most central premises:

Reflexivity dominates, with nearly twice the centrality of any other premise. Multiplication lemmas rank higher than addition lemmas, reflecting Mathlib's emphasis on abstract algebra where multiplicative notation is primary.

Finding 3: Natural Communities

The Louvain algorithm identifies 493 communities from co-occurrence patterns alone—without any semantic information. These correspond to recognizable mathematical areas:

• Community 1 (1,867 nodes): Polynomials, complex analysis
• Community 2 (1,721 nodes): Measure theory, integration
• Community 3 (1,698 nodes): Combinatorics, cardinality
• Community 4 (1,636 nodes): Limits, functional analysis

The topology of proofs encodes mathematical subject matter.

Finding 4: Short Paths Between Distant Domains

How does Topology connect to Number Theory? The shortest path:

Three hops, through reflexivity. Even distant mathematical domains connect quickly through foundational axioms.

The Predictive Model (and Its Limitations)

I trained an XGBoost classifier to predict whether a premise is "high utility" (top 10% by usage). Features: degree, clustering coefficient, community ID.

• AUC-ROC: 0.9791
• Accuracy: 0.9614

This appears impressive until one examines feature importance:

• Degree: 0.892
• Clustering Coefficient: 0.060
• Community ID: 0.049

Degree accounts for 89% of predictive power. Degree alone achieves 97.79% AUC. The relationship is nearly tautological: a premise used in many proofs will co-occur with many other premises, mechanically increasing its degree. The model is essentially predicting usage from a correlate of usage.

Finding 5: Usage Gap Anomalies

The model's value lies not in prediction but in identifying anomalies. I computed, for each premise, the difference between its actual usage and the expected usage for premises of similar degree. Large gaps indicate premises that are well-connected but underused:

tsum_le_tsum—the monotonicity of infinite sums—is used 86 fewer times than its connectivity would suggest. It is the largest anomaly in Mathlib.

For contrast, HasFDerivAt (the Fréchet derivative) was flagged by the model with 91.9% confidence, but its usage gap is 0. It is used exactly as expected for its degree. Not all model predictions indicate true anomalies.

Interpretation

Why might these premises be underused relative to their connectivity?

• Abstraction penalty: General lemmas like tsum_le_tsum may be less convenient than specialized versions for finite sums.
• Type coercion friction: Lemmas like cast_abs and val_zero bridge numeric types; users may avoid explicit casts.
• Discoverability: These lemmas may be poorly documented or absent from common tactics.
• Legitimate alternatives: Other lemmas may serve the same purpose more naturally.

Conclusions

Mathlib, viewed as a network, reveals that:

1. Formalized mathematics is shallow—most premises lie within two steps of rfl.
2. Community structure emerges naturally from proof patterns.
3. Some premises exhibit usage gaps worth investigating.

The predictive model is largely tautological. The structural findings are descriptive, not causal. But the portrait that emerges—of a shallow, modular, rfl-centered mathematical universe—is, I think, worth contemplating.

Graph likelihood

Banerji–Mansour–Severini define the likelihood of a graph \(G\) on \(n\) vertices as the probability that a “monkey” constructs \(G\) in exactly \(n\) steps by adding one vertex per step: at step \(t\) it picks a degree \(k\in\{0,\dots,t-1\}\) uniformly, then picks \(k\) neighbors uniformly among the existing \(t-1\) vertices. The likelihood is \(L(G)=\Pr(G_n \simeq G)\).

Two immediate remarks: (i) the symmetry \(k\leftrightarrow (t-1-k)\) plus \(\binom{t-1}{k}=\binom{t-1}{t-1-k}\) implies \(L(G)=L(\overline{G})\); (ii) the formula is a “partition function over arrival orders”: a sum over all labelings \(\phi\), with a weight that depends only on the back-degrees \(d_t(\phi)\).

A natural generalization

The monkey rule “choose \(k\) uniformly” can be replaced by an arbitrary degree law. Fix distributions \(p_t\) on \(\{0,\dots,t-1\}\). At step \(t\), first draw \(K_t\sim p_t\), then choose a \(K_t\)-subset uniformly. The same derivation yields

Complement-invariance now holds iff each \(p_t\) is symmetric: \(p_t(k)=p_t(t-1-k)\). A pleasant special case is the binomial choice \(p_t(k)=\binom{t-1}{k}q^k(1-q)^{t-1-k}\), which makes every subset \(S\subseteq[t-1]\) appear with probability \(q^{|S|}(1-q)^{t-1-|S|}\). In that case the labeled distribution is exactly \(G(n,q)\), and the unlabeled likelihood becomes \[ L_{p}(G)=\frac{n!}{|\mathrm{Aut}(G)|}\,q^{m}(1-q)^{\binom{n}{2}-m}, \] where \(m=|E(G)|\).

References

C. R. S. Banerji, T. Mansour, S. Severini, A notion of graph likelihood and an infinite monkey theorem, arXiv:1304.3600 (2013; published in J. Phys. A).  —  D. Dervovic, A. Mocherla, S. Severini, Constructing graphs with limited resources, arXiv:1802.09844 (2018).  —  S. Janson, S. Severini, An example of graph limits of growing sequences of random graphs, Journal of Combinatorics 4(1):67–80 (2013).