DeepMind's latest reasoning model ProofZero achieved gold on the IMO in mid-2025. It went on to make its seminal contribution in early 2026 with a complete, verifiable proof of the abc conjecture. Spanning a million lines of Lean, the proof validated Shinichi Mochizuki's Inter-universal Teichmüller theory, with key bridging insights finally making it accessible to the broader mathematical community. Mochizuki, now semi-retired in Kyoto, dismissed the AI's contribution, insisting his original proof was complete.
You got the first part right, so I'm now eagerly awaiting the second part to also turn out right in a couple months' time...
1Your phrasing seems to assume Mochizuki is the one skeptical of formalisation (the quote is from Boyd, not Mochizuki). Mochizuki himself really wants formalisation and is actively involved in various related efforts, e.g. Section 3.2 of his report (all emphasis his):
I have also been deeply impressed and encouraged by the entirely unanticipated enthusiasm that has been exhibited in recent years by computer scientists deeply involved with the development of Lean who are not mathematicians, and whose work has no direct connections to arithmetic geometry (hence, a fortiori, to IUT!), but who have expressed a keen interest in learning more about the situation surrounding IUT and, in particular, investigating what can be done with regard to pursuing the goal of Lean-style formalization of IUT. Such computer scientists, despite being disconnected from the mathematical community in a strict professional sense, nevertheless have substantial personal interaction with professional mathematicians, and it is through such personal connections that this enthusiasm was communicated to me. Moreover, as a result of these ties between the Lean-development community and the mathematical community, I have been invited to give an online talk on the topic of Lean-style formalization of IUT at a workshop on formalization that has been scheduled to be held in the spring of 2026 in the United Kingdom.
Great spot check!
What we really care about is the expected cost to prevent AI extinction via donating to political candidates.
I commented the following on Eric's post, which is as close as I can get to what you asked for:
I really appreciate your explicit cost-effectiveness estimate figures ($85-105k per +1% increment in win prob & 2 basis points x-risk reduction if he wins → $4-5M per basis point which looks fantastic vs the $100M per basis point bar I've seen for a 'good bet' or this $3.5B per basis point ballpark willingness to pay)
(The basis points remark comes from this section.)
Yeah wonder what Tabarrok meant by that, he'd obviously know this.
You know how to walk. When did you last think about contracting your quads?
This reminded me of this line from Peter Watts' Blindsight, which seems relevant:
A memory rose into my mind and stuck there: a man in motion, head bent, mouth twisted into an unrelenting grimace. His eyes focused on one foot, then the other. His legs moved stiffly, carefully. His arms moved not at all. He lurched like a zombie in thrall to rigor mortis.
I knew what it was. Proprioreceptive polyneuropathy, a case study I'd encountered in ConSensus back before Szpindel had died. This was what Pag had once compared me to; a man who had lost his mind. Only self-awareness remained. Deprived of the unconscious sense and subroutines he had always taken for granted, he'd had to focus on each and every step across the room. His body no longer knew where its limbs were or what they were doing. To move at all, to even remain upright, he had to bear constant witness. ...
This is the best that consciousness can do, when left on its own.
A sad example of what Scott Aaronson called bureaucratic blankface: Hannah Cairo, who at 17 published a counterexample to the longstanding Mizohata-Takeuchi conjecture which electrified harmonic analysis experts the world over, decided after completing the proof to apply to 10 graduate programs. 6 rejected her because she didn't have a graduate degree nor a high school diploma (she'd been advised by Zvezdelina Stankova, founder of the top-tier Berkeley Math Circle, to skip undergrad at 14 and enrol straight in grad-level courses as she'd already taught herself an advanced undergrad curriculum by then from Khan Academy and textbooks). 2 admitted her but were then overridden by administrators. Only the U of Maryland and John Hopkins overlooked her unconventional CV. This enraged Alex Tabarrok:
Kudos to UMD and JHU! But what is going on at those other universities?!! Their sole mission is to identify and nurture talent. They have armies of admissions staff and tout their “holistic” approach to recognizing creativity and intellectual promise even when it follows an unconventional path. Yet they can’t make room for a genius who has been vetted by some of the top mathematicians in the world? This is institutional failure.
We saw similar failures during COVID: researchers at Yale’s School of Public Health, working on new tests, couldn’t get funding from their own billion-dollar institution and would have stalled without Tyler’s Fast Grants. But the problem isn’t just speed. Emergent Ventures isn’t about speed but about discovering talent. If you wonder why EV has been so successful look to Tyler and people like Shruti Rajagopalan and to the noble funders but look also to the fact that their competitors are so bureaucratic that they can’t recognize talent even when it is thrust upon them.
It’s a very good thing EV exists. But you know your city is broken when you need Batman to fight crime. EV will have truly succeeded when the rest of the system is inspired into raising its game.
On blankfaces, quoting Scott:
What exactly is a blankface? He or she is often a mid-level bureaucrat, but not every bureaucrat is a blankface, and not every blankface is a bureaucrat. A blankface is anyone who enjoys wielding the power entrusted in them to make others miserable by acting like a cog in a broken machine, rather than like a human being with courage, judgment, and responsibility for their actions. A blankface meets every appeal to facts, logic, and plain compassion with the same repetition of rules and regulations and the same blank stare—a blank stare that, more often than not, conceals a contemptuous smile.
The longer I live, the more I see blankfacedness as one of the fundamental evils of the human condition. Yes, it contains large elements of stupidity, incuriosity, malevolence, and bureaucratic indifference, but it’s not reducible to any of those. ...
Update (Aug. 3): Surprisingly many people seem to have read this post, and come away with the notion that a “blankface” is simply anyone who’s a stickler for rules and formalized procedures. They’ve then tried to refute me with examples of where it’s good to be a stickler, or where I in particular would believe that it’s good. But no, that’s not it at all. ...
Here’s how to tell a blankface: suppose you see someone enforcing or interpreting a rule in a way that strikes you as obviously absurd. And suppose you point it out to them.
Do they say “I disagree, here’s why it actually does make sense”? They might be mistaken but they’re not a blankface.
Do they say “tell me about it, it makes zero sense, but it’s above my pay grade to change”? You might wish they were more dogged or courageous but again they’re not a blankface.
Or do they ignore all your arguments and just restate the original rule—seemingly angered by what they understood as a challenge to their authority, and delighted to reassert it? That’s the blankface.
1
1
1Seems like you missed the point of the post? Last 2 paragraphs
Knowing how to perform a task yourself at all is not the same as knowing how to perform it as well as the person you are delegating the task to. The goal is not to ensure that competence across every work-relevant dimension strictly declines as you go down the organizational hierarchy. You frequently will, and should, delegate to people who are 10x faster, or 10x better at a task than you are yourself.
But by knowing how to perform a task yourself, if slowly or more jankily than your delegees, you will maintain the ability to set realistic performance standards, jump in and keep pushing on the task if it becomes an organizational bottleneck, and audit systems and automations that are produced as part of working on the task. This will take you a bunch of time, and often feel like it detracts from more urgent priorities, but is worth the high cost.
I like Greg Egan's "outlooks" from Diaspora for many reasons: as a reversible customisable solution to value drift, as a way to temporarily experience the world from the perspective of people with very different aesthetic sensibilities or deep values, to approach problem-solving differently, maybe even to simulate high-level generators of disagreement (which would be a boon for erisology), and I wish it already existed:
Any citizen with a mind broadly modeled on a flesher's was vulnerable to drift: the decay over time of even the most cherished goals and values. Flexibility was an essential part of the flesher legacy, hut after a dozen computational equivalents of the preIntrodus lifespan, even the most robust personality was liable to unwind into an entropic mess. None of the polises' founders had chosen to build predetermined stabilizing mechanisms into their basic designs, though, lest the entire species ossify into tribes of self-perpetuating monomaniacs, parasitized by a handful of memes.
It was judged far safer for each citizen to be free to choose from a wide variety of outlooks: software that could run inside your exoself and reinforce the qualities you valued most, if and when you felt the need for such an anchor. The possibilities for short-term cross-cultural experimentation were almost incidental.
Each outlook offered a slightly different package of values and aesthetics, often built up from the ancestral reasons-to-be-cheerful that still lingered to some degree in most citizens' minds: Regularities and periodicities--rhythms like days and seasons. Harmonies and elaborations, in sounds and images, and in ideas. Novelty. Reminiscence and anticipation. Gossip, companionship, empathy, compassion. Solitude and silence. There was a continuum which stretched all the way from trivial aesthetic preferences to emotional associations to the cornerstones of morality and identity.
and further down:
Inoshiro had argued that this was vis last chance to do anything "remotely exciting" before ve started using a miner's outlook and "lost interest in everything else"--but that simply wasn't true; the outlook was more like a spine than a straitjacket, a strengthened internal framework, not a constrictive cage.
One example is miners (of mathematical truth) using outlooks "to keep themselves focused on their work, gigatau after gigatau" (a gigatau is a billion subjective seconds or ~31 years; even among what Mumford calls detective-type mathematicians like Andrew Wiles of FLT fame that's not the norm). Another example is for appreciating otherwise-incomprehensible art:
"Come and see Hashim's new piece."
"Maybe later." Hashim was one of Inoshiro's Ashton-Laval artist friends. Yatima found most of their work bewildering, though whether it was the interpolis difference in mental architecture or just vis own personal taste, ve wasn't sure. Certainly, Inoshiro insisted that it was all "sublime."
"It's real time, ephemeral. Now or never."
"Not true: you could record it for me, or I could send a proxy-"
Ve stretched vis pewter face into an exaggerated scowl. "Don't he such a philistine. Once the artist decides the parameters, they're sacrosanct-"
"Hashim's parameters are just incomprehensible. Look, I know I won't like it. You go."
Inoshiro hesitated, slowly letting vis features shrink back to normal size. "You could appreciate Hashim's work, if you wanted to. If you ran the right outlook."
Yatima stared at ver. "Is that what you do?"
"Yes." Inoshiro stretched out vis hand, and a flower sprouted from the palm, a green-and-violet orchid which emitted an Ashton-Laval library address. ...
Yatima sniffed the flower again, warily. The Ashton-laval address smelt distinctly foreign ... but that was just unfamiliarity. Ve had vis exoself take a copy of the outlook and scrutinize it carefully. ... Yatima had vis exoself's analysis of the outlook appear in the scape in front of ver as a pair of before-and-after maps of vis own most affected neural structures. The maps were like nets, with spheres at every junction to represent symbols; proportionate changes in the symbols' size showed how the outlook would tweak them.
"Death' gets a tenfold boost? Spare me."
"Only because it's so underdeveloped initially." ...
"Make up your mind; it's starting soon."
"You mean make my mind Hashim's?" "Hashim doesn't use an outlook." ...
Vis exoself's verdict on the potential for parasitism was fairly sanguine, though there could he no guarantees. If ve ran the outlook for a few kilotau, ve ought to be able to stop.
Yatima ran the outlook. At once, certain features of the scape seized vis attention: a thin streak of cloud in the blue sky, a cluster of distant trees, the wind rippling through the grass nearby. It was like switching from one gestalt color map to another, and seeing some objects leap out because they'd changed more than the rest. After a moment the effect died down, but Yatima still felt distinctly modified; the equilibrium had shifted in the tug-of-war between all the symbols in vis mind, and the ordinary buzz of consciousness had a slightly different tone to it.
"Are you okay?" Inoshiro actually looked concerned, and Yatima felt a rare, raw surge of affection for ver. Inoshiro always wanted to show ver what ve'd found in vis endless fossicking through the Coalition's possibilities--because ve really did want ver to know what the choices were.
"I'm still myself. I think."
"Pity." Inoshiro sent the address, and they jumped into Hashim's artwork together.
An example of a bad outlook in Diaspora is the one the Ostvalds use which "made them lap up any old astrobabble like this as if it was dazzlingly profound". And here's what I'd consider a horrifying outlook, like a monstrous perversion of enlightenment, which Inoshiro applied to verself after a severely traumatic experience:
Inoshiro said, "I feel great compassion for all conscious beings. But there's nothing to be done. There
will always be suffering. There will always be death." ...Yatima tried to read vis face, but Inoshiro just gazed back with a psychoblast's innocence. "What's happened to you? What have you done to yourself?"
Inoshiro smiled beatifically and held out vis hands. A white lotus flower blossomed from the center of each palm, both emitting identical reference tags. Yatima hesitated, then followed their scent. It was an old outlook, buried in the Ashton-Laval library, copied nine centuries before from one of the ancient memetic replicators that had infested the fleshers. It imposed a hermetically sealed package of beliefs about the nature of the self, and the futility of striving ... including explicit renunciations of every mode of reasoning able to illuminate the core beliefs' failings.
Analysis with a standard tool confirmed that the outlook was universally self-affirming. Once you ran it, you could not change your mind. Once you ran it, you could not be talked out of it.
Yatima said numbly, "You were smarter than that. Stronger than that." But when Inoshiro was wounded by Lacerta, what hadn't ve done that might have made a difference? That might have spared ver the need for the kind of anesthetic that dissolved everything ve'd once been?
Inoshiro laughed. "So what am I now? Wise enough to be weak? Or strong enough to be foolish?"
"What you are now-" Ve couldn't say it.
What you are now is not Inoshiro.
Yatima stood motionless beside ver, sick with grief, angry and helpless. Ve was not in the fleshers' world anymore; there was no nanoware bullet ve could fire into this imaginary body. Inoshiro had made vis choice, destroying vis old self and creating a new one to follow the ancient meme's dictates, and no one else had the right to question this, let alone the power to reverse it.
My interest in Egan's outlooks is motivated by real-world examples too. The example I always think about is Scott's observation that compared to a decade ago he's trended "more cynical, more mellow, and more prone to believing things are complicated" and posits (among others) that it would suck if "everything we thought was “gaining wisdom with age” was just “brain receptors consistently functioning differently with age”", like NMDA receptor function changing with aging and maybe "the genes for liberal-conservative differences are mostly NMDA receptors in the brain" (to give a simplistic illustrative example he doesn't actually put credence in).
The most salient motivating example at the moment is different, it's Cube Flipper's estrogen trip report, which I find fascinating, especially these parts (to summarise their wonderfully-detailed descriptions):
- sense of space around them was "as if I took the entire volumetric representation of the space around me and increased the degree to which every point within that could influence the location of every other point, recursively. This allows everything to elastically settle into a more harmonious equilibrium", which made e.g. parallel parking in particular and driving in general easier
- sweet things tasted sweeter, sour things "tasted both sweeter and more metallic"
- funny things were funnier, "music works now", they can "lean in to the sense of affection they feel towards their friends", but also they've had situations which they felt compelled to do something about instead of being able to healthily dissociate
- wide variation in the way boys smelled, sometimes really quite unpleasant
- a sense that their body map was reshaped, "smoothing out knots – like an elastic membrane being tightened, or a soap bubble reaching equilibrium"; might be what others mean by feeling more embodied
And this summary of changes, from a section where the author investigates whether estrogen was pushing them towards the other end of the "autism-schizotypy continuum" by reducing inherent oversensitivity to sensory prediction errors:
I’ll outline some of the psychological changes I’ve noticed in myself since starting estrogen. ...
- Increased predisposition towards associative thinking. Activities like tarot are more appealing.
- Increased predisposition towards magical thinking, leading to some idiosyncratic worldviews. This can probably be gauged by the nonsense I post on Twitter.
- Increased experience of meaningness in day-to-day life. This felt really good.
- Increased mentalising of other people’s internal states, resulting in a mixture of higher empathy and higher social anxiety. I’m somewhat more neurotic about potential threats.
- Decreased sensory sensitivity.
- Decreased attentional diffusion, contrary to what the paper predicts.
- Decreased systematising and attention to detail, for instance with tedious matters like finances.
Armchair diagnoses aside, I do wish to assert that these psychological changes are quite similar to the kind of psychological changes I tend to experience while on a mild dose of psychedelics.
(Tangentially this seems very relevant to the whole high-decoupling vs high-contextualising thing.)
Egan's outlooks would be like the far more sophisticated version of this: higher precision and customisability (e.g. "death-salience only", or "don't lose interest in everything else" cf. the miner outlooks above), higher control granularity (onset/reversal timescales etc), predictable return to baseline, predictability & previewability of changes (and also non-individual variability).
1Interesting anecdotes from an ex-SpaceX engineer who started out thinking "Elon's algorithm" was obviously correct and gradually grew cynical as SpaceX scaled:
Questioning the requirements was an extremely literal thing that you were supposed to do multiple times every single day. I’d make a claim about my system (“hey, if the stuff in this tube gets too hot, my part will explode, so please don’t put anything too hot near it”) and that very afternoon three or four people would stop by my desk, ready to debate.
“Hello,” they would say. “I’m the Responsible Engineer for the Hot Things Near Tubes system,” and then the floodgates would open. What did I mean by near? What did I mean by hot? How hot was too hot? Was it really going to explode? If it exploded, was that really so terrible?
The first time, the debate would be interesting. The second, it would be a bit tiresome. By the first week after a new claim, it was exhausting and a little rote. But you had to win, every time, because if you didn’t, nobody would follow your requirement.
It also worked in the other direction. I learned to pay attention to everything that was happening in the whole program, absorbing dozens of update emails a day, because people would announce Requirements, and I’d need to go Question Them. If I didn’t do this, I’d find my system forced to jump through too many hoops to work, and, of course, I would be Responsible. If I was Responsible for too many things, I wouldn’t be able to support all of them - unless, of course, I managed to Delete the Part and free myself from one of those burdens.
And so when there were requirements, they were strong, because they had to survive an endless barrage of attack. When there were parts, they were well-justified, because every person involved in the process of making them had tried to delete them first. And there were no requirements matrices, no engineering standards, practically no documentation at all.
The key point came in, the reason why it was capitalized. It wasn’t philosophy, it wasn’t advice - it was an Algorithm. A set of process steps that you followed to be a good engineer. And all of us good engineers were being forced by unstoppable cultural forces to maniacally follow it.
There was one question slowly building in my mind. The point of SpaceX was to get good engineers, do first principles analysis, let them iterate, and avoid documentation. This whole process was clearly succeeding at the last three steps. But if we were already so great, why did we have to have this process enforced so aggressively?
As the time went on and the Algorithm grew, screaming ever-louder about what we should specifically do, the question grew more ever more urgent.
Tell people to ritualize Questioning Requirements and they will do so ritually. You’ll deliver the same explanation for how hot your tube can be a hundred times, and each time you deliver it you think about it less. You will realize that the best way to get work done is to build a persona as extremely knowledgeable and worthless to question, and then nobody ever questions your work.
Tell people to Delete the Part, and they’ll have the system perform ridiculous gymnastics in software to avoid making a 30$ bracket, or waste performance to avoid adding a process.
Tell people to Optimize the Part and they’ll push it beyond margins unnecessarily, leaving it exquisite at one thing and hopeless at others.
Tell them to Accelerate, and they’ll do a great job of questioning, but when push comes to shove they will always Accelerate at the cost of quality or rework, and so you find yourself building vehicles and then scrapping them, over and over again.
There is no step for Test in the Algorithm, no step for “prove it works.” And so years went by where we Questioned, and Deleted, and Optimized, and Accelerated, and Automated, and rockets piled up outside the factory and between mid-2021 and mid-2023 they never flew.
Every engineer was Responsible for their own part. But every engineer had perverse incentives. With all that Accelerating and Automating, if my parts got on the rocket on time, I succeeded. In fact, if the rocket never flew, I succeeded more, because my parts never got tested.
And so we made mistakes, and we did silly things. The rocket exploded a lot, and sometimes we learned something useful, but sometimes we didn’t. We spent billions of dollars. And throughout it all, the program schedule slid inexorably to the right.
And I got cynical.
There were enormous opportunities to have upside improvement in the rocket industry of the 2000s and 2010s. The company was small and scrappy and working hard. The rules applied.
But by the 2020s, even SpaceX was growing large. The company had passed 10,000 people, with programs across the country, tendrils in every major space effort and endlessly escalating ambition.
And the larger it became, the greater the costs to its architecture became. As my program grew from dozens of people to hundreds to thousands, every RE needed to read more emails, track more issues, debate more requirements. And beyond that, every RE needed to be controlled by common culture to ensure good execution, which wasn’t growing fast enough to meet the churn rate of the new engineers.
This makes me wonder if SpaceX could actually be substantially faster if it took systems engineering as seriously as the author hoped (like say the Apollo program did), overwhelmingly dominant as they currently are in terms of mass launch fraction etc. To quote the author:
The first recorded use of the term “Systems Engineering” came from a 1950 presentation by Mervin J. Kelly, Vice President of Bell Telephone. It appeared as a new business segment, coequal with mainstays like Research and Development. Like much of the writing on systems engineering, the anodyne tone hid huge ambition.
‘Systems engineering’ controls and guides the use of the new knowledge obtained from the research and fundamental development programs … and the improvement and lowering of cost of services…’
In other words, this was meta-engineering.
The problems were too complex, so the process had to be a designed thing, a product of its own, which would intake the project goals and output good decision making.
It began with small things. There should be clear requirements for what the system is supposed to do. They should be boxed out and boiled down so that each engineer knows exactly what problem to solve and how it impacts the other ones. Changes would flow through the process and their impacts would be automatically assessed. Surrounding it grew a structure of reviews, process milestones, and organizational culture, to capture mistakes, record them, and make sure nobody else made them again.
And it worked! All of those transcendental results from Apollo were in fact supported on the foundations of exquisitely handled systems engineering and program management. The tools developed here helped catapult commercial aviation and sent probes off beyond the Solar System and much more besides.
At SpaceX, there was no such thing as a “Systems Engineer.” The whole idea was anathema. After all, you could describe the point of systems engineering, and process culture more generally, as the process of removing human responsibility and agency. The point of building a system to control human behavior is that humans are fallible. You write them an endless list of rules to follow and procedures to read, and they follow them correctly, and then it works out.
At SpaceX, it wasn’t going to be like that. First principles thinking and Requirements Questioning and the centrality of responsible engineering all centered around the idea of raising the agency of each individual engineer. Raising individual responsibility was always better.
Interesting, why do you have a lot of uncertainty on #4?