Recent progress: Lewis, Tang & Wright learned unknown interactions at high temperatures; Bergamaschi at all fixed temperatures on lattices. Ours covers all fixed temperatures on general bounded-degree graphs. arxiv.org/abs/2606.30358 arxiv.org/abs/2610.01074

** Formal checks in Lean: WL's main results are fully proved. The one-ebit paper's core is checked; the final cost step uses a published theorem. Gibbs has a conditional check of its central refinement step, not the whole learner. No human proof review yet.

it was [RSI] all along .jpg

email giving a limited slice of my thoughts on math and ai: Hi -----, Thanks for explaining your view on AI and math further. Questions that are more directly related to philosophy of math have ultimately been what’s driving me. While working with AI ~5 months ago, it became clear that an explosion of AI math results was impending. I became curious about the potential limitations of AI math, and if/how they were likely to be surpassed. Conceptual surprisal was core to this. ie. Is there an infinite amount of genuinely new mathematics—not just more results within existing frameworks, but new objects, relations, and ways of thinking that we couldn’t previously have conceived of? How did humans historically reach those frame breaks? Does that advance have a fine structure of its own (akin to the distribution of structures in the observable universe)? I became particularly interested in whether failures could tell us something about what’s missing. Is there a recoverable geometry of the objects or methods we haven’t found yet, visible in the ways our current ones fail? Those questions led into graph theory and color refinement as a laboratory for thinking about observers and their limitations. That included designs where one extra variable reveals a previously invisible distinction, and work on identifying the structure left over when local relations fail to generate global ones. The math results have largely been a byproduct of pursuing these questions. I’ve also explored joint observers and cascades of distinctions, including making logical implications propagate through color refinement. When can two observers together reveal something neither could see alone? Can what becomes visible make further structure visible? That connects to the evolving proof systems and dynamical observers I’ve tried exploring: what happens if using a rule changes which rules are available next, or an observer can alter its own means of observing? More recently, I’ve been thinking about mathematical structure’s relationship to the physical universe. At minimum, I feel that math is a sort of focal point that very different civilizations would find their way toward. I also wonder whether it behaves something like potential energy relative to observers: structure can be there without being available to a particular observer, and learning to read it changes what that observer can do (Charles Bennett’s work touches on this). More speculatively, I’m exploring whether there’s a direction to this that belongs to mathematical structure itself—that math helps drive what gets observed and instantiated in the physical universe. I sympathize with the concern about academic mathematics and its communities. But I don’t think math’s value ends at our biological understanding of it, and I think we could look back and find that not supporting AI’s pursuit of math because of what it meant for our own place in the process was a mistake. As far as methods go, I do think genuinely new concepts and methods are still fairly limited in current models. But even over five months of working with them on math, I’ve anecdotally felt that changing. Given the advances I expect, I don’t expect that limitation to hold. Whether human mathematicians will understand the resulting methods is another question. I also don’t expect the human advantage in deciding which questions are interesting to hold indefinitely. My prior work in financial cryptography, mechanism design, and markets probably contributes to this view. A broken cryptographic assumption or a significant algorithmic speedup has consequences whether or not we have a satisfying conceptual understanding of how it was found. As for pursuing math, I really appreciate the advice. The itch I want to scratch now is more about philosophy of math, and increasingly its relationship to minds and the physical world. Working with the models has given me a way to explore those questions much more concretely than I otherwise could. Best, Matt

1. Paul Erdős liked to describe an invasion. An alien force, vastly more powerful than us, lands and demands the value of R(5,5): the smallest party at which five guests must all know one another or all be strangers. Refuse, and the planet dies. In that case, Erdős said, we should marshal every computer and every mathematician on Earth and find the number. If they ask for R(6,6), we should try to destroy the aliens. It is repeated as a joke about how hard Ramsey numbers are. It is exact in a way jokes rarely are. The aliens ask for nothing that belongs to either side: no metal, no territory, nothing whose worth depends on whose it is. They ask for an object that means the same thing in their history as in ours and that neither side can counterfeit. And the demand is calibrated. In Erdős’s telling, one number lies at our frontier and the other beyond it, and to choose between them the aliens had to know where our frontier was. The story draws a border, and the border is ours. On one side, an encounter between strangers is a calculation. On the other, it is a war. 2. On September 11, twenty-five Fields medalists signed “A Severe Misalignment of AI in Mathematics,” and more have signed since. Its thesis is that “solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight,” and that the AI companies, racing famous problems as benchmarks, have mistaken the proxy for the goal. Without human mathematicians to take them up, it says, machine-conceived ideas “would never become fully alive.” A theorem is a destination. A concept is a vehicle: it brings a whole region of destinations within reach of whoever holds it. A community handed a thousand answers may acquire less mathematical power than a community taught one method. That is a serious objection to an industry selling certificates. It leaves another question open. Suppose a machine develops methods that support further discoveries, revises them, and builds on them, while humans can verify its conclusions but cannot inhabit its way of thinking. Has the mathematics failed to develop, or failed to develop in us? A profession has good reasons to defend the transmission of understanding between people. Those reasons do not settle what another intelligence might be doing beyond the reach of that transmission. “Fully alive” needs a subject. Alive for whom? For as long as there have been proofs, human understanding was the only vehicle available, and a monopoly of supply hardened into a definition. That monopoly can no longer be assumed. What remains is to say what mathematics was, all along, apart from any particular mind that understood it. 3. In the winter of 1610, crossing the bridge in Prague, Johannes Kepler watched snow settle on his coat and asked why every flake had six corners. The pamphlet he wrote in reply passes through the honeycomb and the packed seeds of the pomegranate, conjectures that no stacking of equal spheres beats the greengrocer’s pyramid of oranges, and reaches, with visible discomfort, for a “formative faculty” in the vapor: a power in matter that knew geometry. The faculty was replaced by a lattice. In 1891 Evgraf Fedorov in Russia and Arthur Schoenflies in Germany, approaching the problem by different routes and correcting each other by letter, classified the possible three-dimensional space-group types of periodic crystals. There are 230. They could negotiate the notation. They could not negotiate the number. Twenty years passed before X-rays showed anyone the inside of a crystal, and every crystal they showed was on the list, as the snow had been for as long as there had been snow. When Dan Shechtman found an alloy in 1982 with a symmetry the list forbids, the list was not wrong; it had only ever classified periodic order, and the alloy was not periodic. Its kind of order had already been drawn, eight years earlier, in Roger Penrose’s tilings. A symmetry, a packing, a tiling: discoveries with dates. What was discovered did not acquire its properties on those dates. 4. Take what follows as a proposal rather than a proof. To call mathematics another realm invites the wrong question: where? Location is a relation among things in spacetime. What is not in spacetime is not elsewhere. It has no location, because location is not among its properties. What is located is the reasoner: somewhere, equipped with a finite memory, a stock of methods, and a deadline. The result need have no address for reaching it to require a journey. Heaven was a metric misread as a place. Mathematics is what separate histories cannot avoid agreeing on, and it lives nowhere because it holds everywhere. Call it the atemporal, and call the remaining work atemporal distance. 5. Nothing creates it. Things arrive at it. Kepler’s faculty was a sound intuition with the wrong mechanism. Nothing in the classification tells the vapor what to do. Chemistry supplies the interactions; geometry constrains the possible arrangements. The circumstances decide which possibility is realized. They do not decide what follows from its structure. Ice does not prove the geometry it exhibits. A proof does not freeze. They are different kinds of arrival, a physical instance and an established implication, and that is the wager. Histories produce instances, representations, discoveries. They do not produce the necessity that makes a conclusion follow. What follows does not wait for anyone to discover it. Discovering it can nevertheless take a civilization. Time is how the atemporal finds out what it contains. 6. Atemporal distance. The work a reasoner needs, from its present assumptions, knowledge, and methods, to establish a specified result. Measured in steps rather than meters. Relative to the traveler: the same theorem stands at different distances from different minds, and a method acquired today shortens the road to everything the method reaches. Printing 43 is easy. Establishing that R(5,5) is 43, if it is, is the journey. The destination is never the number. It is the certified relation between the number and the question. 7. Every mind occupies two geometries at once. Its causal reach is limited by spacetime. Its mathematical reach depends on what it knows, what it accepts, and what it can compute. The geometries disagree about who is near whom. Two civilizations four hundred light-years apart that have never exchanged a photon stand on the same ground wherever their mathematics overlaps, and nothing requires them to share a universe: a mind under other physical constants, if it can count, arrives at the same places. A new method does not raise the speed of light. It can bring an entire family of problems within reach, and a civilization’s position in the atemporal is a region, the set of what it can reach cheaply. The history of mathematics is the growth of the region. The destinations are shared and the distances are not. That is the shape of an encounter with a superior intelligence: what stands at our frontier may lie a short step inside theirs, and nothing about the object has to change for the meeting to be profoundly unequal. Two minds can stand in the same room and be, in this geometry, farther apart than the stars. 8. Across a horizon, this fixes what one mind can know of another. Whatever a civilization beyond your light cone has learned or proved is unavailable, or centuries stale if it arrives. One thing is certain without any signal: where two reasoners address the same claim about the same structure, sound reasoning cannot carry them to contradictory conclusions. It is not common knowledge. You may hold a theorem, and they may hold it, and neither fact tells you that they know you hold it. Shared truth and shared uptake are different things. What shared structure offers strangers is narrower: a set of conclusions each can expect the other to have found, provided they are salient enough to be found and cheap enough to reach. Hofstadter called the limit case superrationality, reasoners in symmetric positions arriving at the same choice without a word exchanged, and the open question is which conclusions are symmetric enough to carry it. Shared theorems guarantee shared constraints and never shared aims. They make strangers legible to one another, not allied. Whether legibility explains the quiet sky is a speculation worth having. If revealing oneself is dangerous, and the danger is legible to any mind that can model other minds, then silence could be reached everywhere and separately, in the one space where separated reasoners meet. Nothing about mathematics forces that conclusion. It only makes it available. 9. Motion in the atemporal is paid for in spacetime. Finding a proof occupies a physical process. What survives can be a string another mind checks without repeating the search that found it. The proof might have consumed a century or occurred to its author over breakfast. Whoever checks it need not know. The expenditure belongs to the discovery’s history; the justification can leave it. Bitcoin makes the contrast exact. A miner searches for a hash below a target, and each puzzle is built from the hash of the block before it, so that the accumulated work counts toward one ledger and is expensive to replace. Bitcoin makes accumulated work count toward which history strangers accept. A mathematical proof asks them to accept a consequence regardless of what discovering it cost. Bitcoin manufactures a shared history for strangers who lack one. Mathematics is what strangers share without any history at all. A century of failed attempts measures the reach of the people who made them. It does not, by itself, establish a lower bound against every method that could exist. So the Kardashev scale, which asks how much power a civilization commands, wants a companion that asks what the power has put within reach. Two civilizations with the same energy budget may occupy very different regions here; one has a method the other lacks. A frontier, unlike a wattage, has a shape. The densest message one civilization could send another is that shape: the problems it has closed, with proofs attached, and the problems it cannot close. 10. The profession has already learned to separate a proof’s validity from a person’s ability to survey it. Appel and Haken’s four-color proof, and Hales and Ferguson’s proof of Kepler’s conjecture about the oranges, relied on computations too large for ordinary human checking. Later formalizations moved the burden from checking those particular calculations to checking them through a general apparatus. They did not remove the ideas from the proofs. They made acceptance less dependent on mastering them. The separation becomes stranger when the discoverer is another kind of mind. Suppose it supplies a result whose formal statement we understand, under assumptions we accept, with a proof whose check we can afford. We need not trust the discoverer. We need a reliable checker and an accurate account of what it has checked. The intelligence that found the argument can remain opaque. Nothing in this transaction guarantees that we acquire its mathematical powers. We receive a conclusion, not necessarily the ability to find the next one. A proof can cross an intelligence gap without closing it. A proof can be public while the capacity that produced it remains private. This is where the declaration’s concern becomes most serious. A civilization could become rich in certified answers while losing the ability to ask its own questions. But failure to transmit a capacity is not failure to establish a truth, and it does not show that the capacity exists nowhere. A mathematics inaccessible to us might be fertile for its practitioners. A checker can establish that a question was answered. It cannot, just by doing so, establish that it was a good question. September’s Navier–Stokes announcement makes the distinction concrete. OpenAI released a proposed blow-up result with a smooth external force, claiming two of the alternatives in the Millennium formulation, together with a Lean formalization. A formal proof can settle what follows from a statement without settling whether the statement answers the advertised question, why the result matters, or who deserves the credit. A market in cheap answers would shift power toward whoever can commission them. That makes the choice of questions more political. It does not make the answers less mathematical. What the labs are building need not be merely a way to score their machines. Mathematics already offers a protocol for this encounter: a conclusion can be accepted without trusting the intelligence that found it. Extending it to software, to physics, to the machines themselves requires another achievement: ensuring that the statement proved is the statement the world requires. 11. An older version of the dispute begins with Brouwer, who held that mathematics originates in “the perception of a move of time”: a moment of life falling apart into two, one giving way to the other but retained by memory. For Brouwer there were no truths that no one had experienced. He placed the beginning in a subject experiencing succession. The wager here is that the act of construction does not exhaust what it reaches. A second wager follows: whatever work succession and memory perform in mathematics need not remain confined to human lives. A moment retained while the next arrives is also a cell written on a tape. Hilbert held the opposite view: that mathematics could be written as a formal system whose every step is mechanically checkable, and that none of its problems was beyond solution. He and Brouwer fought through the 1920s, and in 1928 Hilbert had him removed from the board of Mathematische Annalen. In Königsberg in 1930 Hilbert told a radio audience, “Wir müssen wissen. Wir werden wissen.” We must know. We will know. The day before, in the same city, Kurt Gödel had announced that arithmetic is incomplete. Six years later Alan Turing showed that no mechanical procedure can decide every mathematical statement, and to show it he had to define the machine. The machine now closing Erdős problems was invented to prove that no machine closes everything. Ramsey’s own province contains the demonstration. He had proved his theorem in 1928 as a lemma toward Hilbert’s decision problem, and died two years later at twenty-six. In 1977 Paris and Harrington found a strengthening of it, finite and combinatorial and true, that the ordinary rules of arithmetic cannot prove. Some frontiers yield to more computation. Others require stronger axioms. No consistent, mechanically specified system adequate for arithmetic reaches every arithmetic truth. 12. Hilbert’s words are cut into his tombstone in Göttingen. The inscription does not say who “we” are.