“Are we justified in assuming a model of nature for which no calculable simulation is possible?”
— Zuse

I don’t remember exactly when I first read Licklider’s 1960 masterpiece, but I’ve been deeply obsessed with his vision ever since. And while I’m not entirely sure, I think it contributed to my early curiosity about AI. He dreamed of a future in which humans and computers would be “very tightly coupled,” a partnership that would “think as no human brain has ever thought.” After more than sixty years, I feel like we’re finally seeing the threads of that symbiotic future unravel, especially in that most abstract of human endeavors: mathematics. The very culture of mathematical formalism, the way we discover, communicate, and even feel mathematical truth, is undergoing a tectonic shift, and it’s all because of the tools we build.

I recently discovered, via Tao’s blog, a paper by Heather Macbeth that was very relevant, articulating much of what was on my mind. She explores deeply the stylistic and philosophical chasms that separate traditional prose mathematics from its increasingly common computer-formalized counterpart. In the old world of pen and paper, intellectual courage is complemented by a pragmatic recognition of the cognitive overload it places on the reader, and by the painstaking work required to ensure that a sweeping abstraction does not hide a fatal flaw or, equally badly, make fundamental intuition opaque. But, as Macbeth points out, these barriers largely dissolve within a formal framework. When presented with a computerized mathematical argument, as a reader I can instantly inspect definitions, trace the origin of a lemma, or check by clicking whether a statement is indeed valid in the precise abstract context it claims to be. The machine handles the meticulous, often laborious bookkeeping. As a programmer of mathematics — a role Licklider would probably have relished — I feel liberated. As I rise above the drudgery of symbol-shuffling and mechanical calculation, I focus my energy on the grand architecture of an argument. I trust that the machine will handle the low-level joins with a precision that far exceeds my own fallible working memory and attention. This reminds me of Perlis’ wonderfully insightful observation:

“You think you know when you learn, are more sure when you can write, even more when you can teach, but certain when you can program.”

When we can articulate a mathematical idea with such clarity that a machine can parse and verify, our own understanding crystallizes, achieving a new, almost unnerving, level of certainty.

This man-computer symbiosis is precisely what Licklider was getting at:

“men will set the goals, formulate the hypotheses, determine the criteria, and perform the evaluations. Computing machines will do the routinizable work that must be done to prepare the way for insights and decisions in technical and scientific thinking.”

And the beauty of this, as Macbeth suggests, is that this partnership leads to a richer, more structured form of mathematical storytelling. We can now easily weave together various forms of mathematical reasoning without disrupting the narrative flow or eroding the trust between author, reader, and the increasingly indispensable machine. I wrote this last year, after a long day of programming:

I’m genuinely happy to see a mathematician of Terence Tao’s caliber vibe coding Python libraries to gain back in thinking what he used to lose in days or weeks of his life. It’s not elegant, he admits, but “elegance is not the point here; rather, that it is automated.” His initial tool quickly evolves into a more general “flexible proof assistant,” explicitly designed to mirror some of the interactive features of mature systems like Lean and SymPy. So here lies Licklider’s symbiosis blooming into something almost Heideggerian, ready-to-hand collaboration, in which the human provides high-level tactics the machine diligently executes through a tedious series of calculations that are ultimately presented as an evolving state of the proof, with human insight and machine rigor together orbiting like a two-body system.

The theme of self-improving systems is something that interests me and I was expecting a pure, AlphaZero-style approach to reasoning in LLMs for quite some time. This paper, in many ways, delivers. The idea is straightforward: completely remove the reliance on human-curated data and forget supervised fine-tuning on mountains of existing proofs or question-answer pairs. A single LLM plays both the role of “proposer” (generating its own mathematical tasks) and the role of “solver.” It dynamically creates its own personalized curriculum, all in a self-play loop, with verifiable rewards coming from the cold, hard truth of code execution. It’s like teaching a child chess by having them invent their own puzzles and then rewarding them for solving them correctly — a daunting, but nonetheless, incredibly rewarding pedagogical strategy (it somehow worked for me). And, remarkably, the authors report the emergence of intermediate planning in the LLM results, a kind of ReAct-style internal monologue that appears in the form of comments and step-by-step logic in the generated code. It’s almost as if the machine is learning to show off its work – “The aim is to outsmart all these groups of intelligent machines and less intelligent humans. This is for the brains behind the future.” – not for a human evaluator, but for itself, slowly bootstrapping toward complex reasoning.

The trajectory from Licklider’s speculative vision to Tao’s LLM-assisted sessions and the self-play of Absolute Zero hides another gem — the pioneering, if perhaps less widely recognized, work of Konrad Zuse. His 1969 treatise, though written decades before the current AI boom, confronted astonishingly prescient questions. Zuse, an engineer by training, was motivated by the practical need to automate computation, but his thinking quickly transcended mere engineering. He posited a universe that was computational, a calculating space assembled from laws of physics explained solely in terms of discrete, automaton-like operations in which concepts like Maxwell’s equations or gravity could be reinterpreted. He imagined “digital particles” and “cellular automata” as fundamental building blocks, wondering whether nature itself could be “digital, analog, or hybrid.” If the universe were really a computer, what would its rules be? He wrote:

“The question therefore appears justified whether data processing can have no more than an effectuating part in the interplay or whether it can also be the source of fruitful ideas which themselves influence the physical theories.”

He wrestled with the philosophical implications for causality and information theory, wondering whether “the assumption of valid determination only in the positive time direction is not influenced in the least by the dissolution of physical laws into the laws of probability.” His reflections on the “information content” of the cosmos and the limits of simulating an infinitely fine reality with finite computational resources seem surprisingly contemporary (just read some of Wolfram’s writings). While his specific models of digital particles might seem primitive today, his fundamental question — “Is nature digital?” — and his attempts to reconcile physics with computational principles laid some of the early foundations for what is now known as digital physics. The very notion that “objects and elementary dimensions of physics must not be complemented by the concept of information, but rather should be explained by it,” as the afterword to the reissue of his work states, is to me a penetrating idea that we should not abandon so lightly.

Today, we are building the tools that Zuse could only dream of, tools that allow us to go beyond simple computation and reason with and about the formal structures of mathematics in entirely new ways. The “software,” to use Zuse’s anachronistic but apt term, is finally starting to catch up with the “hardware” of our mathematical intuitions. Unfortunately, most students still approach mathematics in the same way that early computer scientists wrote assembly code. If I had learned SymPy in high school, I would already be a demigod. Fortunately, the current generation has Claude, so its descendants may well become the demigods of tomorrow.