The heaven button: You wake up one day and find a button in front of you, with a proof next to it. The proof says that pressing the button will kill everyone on the planet and send them all to heaven. Would you press it?
It seems too good to be true. You think it must be a dream. It can't possibly be true. You go through the proof, and it seems correct. But what if you were under the influence of some drug?
But the stakes are very high, so you use software you trust to formalize it in Lean, and you run it on a machine you trust. Lean says the proof is correct so now you are more convinced. But you start doubting yourself again. What if someone compromised the formalization software, or introduced a bug in Lean?
So you check Lean's code, and run the proof on a second machine with an independent checker. It passes again. But each of these checks could fail in the same way the first one could. So you go further and formally verify Lean and the formalization software themselves. They pass. But now you are doubtful of the tool you used to verify this. What if that was compromised by someone? Every new check needs another check behind it, and at some point you have to stop and decide.
Would you press it?
Some people believe that handing control to some general superintelligence would be fine, if we have a formal proof of alignment. That, in my opinion, has similar issues as with the heaven button.
In this post:
First, I present what I think is the hard problem of alignment.
Then I illustrate why testing for alignment is not enough and a proof would be required.
Next, I lay out why a proof could be intractable.
Finally, I argue that, given the risk, even a formal proof that a superintelligence is aligned does not justify its development.
The hard problem of alignment
The hard problem of alignment: How can a system reliably establish whether a system broadly smarter than itself is aligned with it?
The main problem is that a failed test can sometimes show a system is misaligned, but passing every test does not establish that it is aligned.
Note: The question is not whether this is impossible. There may be systems smarter than us at specific tasks whose relative safety we can establish in some sense. The difficulty centres around two terms:
Broadly smarter: I mean smarter in general, as Eliezer Yudkowsky describes it,[1]and not just better at specific tasks like chess. Such a system may end up in control whether or not we hand control over, because we can't count on containing something that out-thinks us.
Reliably establish: I mean to a standard that fits the risk of an irreversible transfer of power, much higher than the one we use for most technologies.
Related work
Related work was put together with help from Claude.
The question is not new, and similar questions have been discussed before.
MIRI studied how an agent can trust a successor that reasons better than it does, under the names tiling agents and Vingean reflection.[2][3]
That a smarter system can behave well until it no longer has to is Bostrom's treacherous turn, and later the work on deceptive alignment.[4][5]
The regress of checking the checker has been discussed for machine-checked proofs by Pollack, and more generally for proof verifiers by Yampolskiy.[6][7]
The gap between a formal proof and the real world has been laid out by Seshia, Sadigh and Sastry, and by Dickson.[8][9]
That a system can shift what we want, instead of satisfying it, has been formalized by Carroll and others.[10]
Part 1: Merely testing can't establish alignment, you would have to prove it
We will use a simple framework to illustrate the difficulty. It is a bit reductive and not a proper formalism of alignment.
Say a system wants to check whether a system is aligned with it. Let be the set of all possible states of the world, and for a state , let be the action in that state that finds desirable. It could also stand for the action that is beneficial for humanity. Let be the action actually takes. For alignment, we would want something like:[11]
With testing, we can only ever check finitely many states, a set . So what a test actually shows is:
It is roughly the state of the art in how frontier labs and many AI safety experts talk about alignment and decide whether it is getting better. A model's system card reports an "alignment assessment," a set of evaluations, and the model is judged against earlier models on how often it behaves badly in them.[12]
To go from to , we need to prove why the behavior should generalize to all states.
Why isn't induction enough? In most industries, it is often enough. We run safety tests and trials, and when a product passes enough of them, we trust it. But if is broadly smarter than , we have to take seriously the possibility that can pass every test can come up with, whether it is aligned or not. Models already sometimes recognize when they are being evaluated, and have behaved differently when they believed they were being trained.[12][13]So we can't rely on induction from to .
We would need to establish holds outside .
Why such proofs could be intractable
1. is not resolved for all states. doesn't know what it wants in most states of the world. Humans disagree with each other and change our minds. So the right-hand side of the equation is not defined for most of .
2. can bring about states we can't reason about. Even if we try to resolve for every situation we can imagine, a system broadly smarter than us can bring about situations that are hard for us to imagine and reason about.
3. can manipulate the target. If can't be fixed in advance, it is open to manipulation. For new situations, what we want would have to be decided later, when they come up. But by then is part of the world we are deciding in, and it can shape what we want, changing the right-hand side instead of the left.
Proposals that try to get around
People have proposed different ways around not being resolved. Roughly, they either hand the job of working out to , or keep us as the judge.
Coherent extrapolated volition (CEV) lets the system work out what we would want if we knew more and were wiser.[14]
Corrigibility doesn't try to fix at all. It asks for a system that lets us correct it or shut it down.[15]
Debate has two systems argue and lets a human judge which one gave the most true and useful information.[16]
I don't think any of them resolve it.
With CEV, does the extrapolating. We could look at the procedure and test some of its outputs, but we are not the wiser, better-informed version of ourselves it is extrapolating to. The further the extrapolation departs from judgments we can make ourselves, the harder it is to establish that it is what we would have wanted, and not just something that looks plausible. So we are back to the problem in Part 1.
Corrigibility and debate keep us in the loop instead of fixing in advance. That helps, but it doesn't remove the problem. Corrigibility tries to make a system accept correction and shutdown without manipulating or resisting us, but the original paper did not fully solve how to do this.[15]Debate tries to help us judge questions we couldn't judge on our own, but it has unresolved problems,[17]and it can only settle the questions we think to ask. In both cases, our judgement is open to manipulation by , as in point 3.
Part 2: Even formalism can't justify superintelligence
Let's assume we get past all of this and have a proof that is aligned. We would still need to verify it. Let be an evaluator working in a formal framework , for example a world model, a safety specification and a verifier, as some guaranteed-safe AI proposals describe.[18]If checks and accepts it:
This is definitely an upgrade from tests, and it would give us considerable trust in . It is also how we already handle some of the highest-stakes systems we build, such as flight control software and secure operating systems, where formal verification is used to prove that the software does what its specification says.
But to reliably establish alignment, we would need a further guarantee that neither nor (nor ) was compromised by in a way that led to the verification passing.
But if we have proven that is aligned, doesn't that already rule this out? No. The passing of the proof was the verification, and we haven't established that the verification itself was intact. Using 's alignment to confirm the proof would be circular.
We can add another check on the evaluator to ensure this. Say checks the integrity of . If the check fails, we find out that something went wrong. But a pass does not rule out that could have been compromised too. So we might need to check , leading to an infinite regress:
Each guarantee needs another guarantee behind it, and there is no point where the chain establishes itself. This is the regress of doubts from the heaven button story, and it applies to basically any proof where we can't establish or ensure a boundary between what is being checked and what is checking it.
There is a second dependency, and more checking does not help with it. A proof is about a model of the system and a model of the world. Whether those models match the real system and the real world is not something the proof can tell us.[8][9]
Core argument: even with a formal proof, we still depend on the verification not having been compromised, and on the formal system matching the real world. Neither of these can be established beyond doubt. And because being wrong here would take away our ability to intervene, the proof is not enough to justify handing over control.
Q: We base our lives on things without absolute guarantees all the time. With your reasoning, it sort of implies there is no such thing as an absolute guarantee, because this regress will apply to any proof.
We have mathematical proofs that hold up, and we use them in high-stakes scenarios. If we had a formal proof that a superintelligent system smarter and more powerful than any of us is aligned to us, why should we not take that?
I agree that there is a spectrum of certainty on which we base our lives. We trust engineers based on their calculations, vaccines based on trials, doctors to cut us open and operate, and our elected governments to make decisions for us.
We trust formal proofs for high-stakes situations. And yes, the regress applies to every proof. I think the question of where we stop checking depends on three things: how much damage being wrong would do, whether it can be reversed, and whether what we are evaluating can influence or manipulate the evaluator.
The consequences of a failure in other technologies, however serious, are relatively contained or reversible. So we accept a certain level of confidence and stop checking. A superintelligence, on the other hand, would be smarter than those evaluating it, and the consequences of getting it wrong could be catastrophic for everyone, with no possibility of reversing the outcome.
When the damage is total, can't be reversed, and the system can influence the check, another layer of checking does not change the decision. The question is no longer how many checks we ran. It is whether we can still intervene if the checks were wrong. Pressing the button, or handing over control, takes away that ability.
I am not questioning the validity of proofs within a formal system. I am pointing to the limitations of formalism when we try to apply it to the real world. Developing general superintelligence could lead to consequences that are irreversible and impact everyone, and we can never have a guarantee that it won't. And building such a system may, at some point, amount to handing over control, whether or not we ever decide to. After that, we can't intervene if we were wrong. Together, these should be the strongest argument against pursuing such systems.
Q: Are you saying that we should not build AI?
No. I am not saying we should stop building AI, and I am not saying a pause is the only safe option. I am saying we should not aim to build AI that is broadly smarter than us.
We should be building AI that makes us more productive, helps us solve hard problems, and moves science forward. I think we should build AI with a focus on amplifying humans,[19]and I think much of what we want from AI can be had this way.
These kinds of AI are not free of the problems in Parts 1 and 2. Formal proofs and a deep understanding of the model can give us relative safety, but tests still can't prove a system is safe, and proofs still rest on assumptions. A system built for specific tasks could also turn out to be more capable than we intended, and we might not notice in time.
So the difference is not that one kind of AI is safe and the other is not. The difference is what happens when we are wrong. If we can still intervene, a mistake is something we can find and correct. With a system broadly smarter than us, we may not get that chance.
That is why we should build AI assuming our own checks could be wrong, and be ready to pause when the risk passes what we are willing to accept. We should never, at any stage, let control slip from humanity on the assumption that alignment will save us.
We don't know how to do this yet. We have no reliable way to tell when a system is getting close to being broadly smarter than us, or to get the benefits of AI while making sure we stay in control. But these are the problems we should be working on, instead of setting broadly smarter intelligence as the goal and working backwards to solve alignment, hoping a formal proof will ensure our safety.
Q: So should one press the button?
My claim is that whatever framework you use, morality, decision theory, rationality, or some other epistemic approach, it should ultimately lead you to conclude that pressing the button is not justified.
I am not an expert in these fields, but it is not a new problem, and several related lines of thought seem to point toward the same conclusion.
Maximin. Rawls argued that when probabilities can't be trusted, when little is lost by playing safe, and when the worst outcomes are unacceptable, it is rational to choose the option with the least bad worst case.[20]
Consent. The button decides for everyone, and not everyone agreed to it.
Flawed arguments. In high-stakes decisions, the chance that an argument itself is flawed can matter more than what it calculates.[21]
Corrupted hardware. Yudkowsky argued that we should not seize power even when it seems to benefit everyone, because our own reasoning might be compromised.[22]
Irreversibility. Arrow and Fisher showed that when a step can't be undone and we expect to learn more, keeping the option open has value of its own.[23]
To me, the fanaticism to build and hand off control to some superintelligence is uncomfortably close to that of an altruistic suicide bomber, who is so convinced by the payoff that they are willing to take a step that can't be undone.
TL;DR
Testing can show that a system is misaligned, but cannot establish that a broadly smarter system will remain aligned outside the situations we test.
A formal proof would be much stronger evidence, but it could be intractable.
Even a formal proof rests on things it cannot establish: the integrity of the proof, verifier and specification, and their connection to the real world.
For most technologies we accept that. For a superintelligence we should not, because being wrong would be irreversible, would affect everyone, and would leave us unable to intervene.
No kind of AI comes with a guarantee, and this is not an argument against building AI. What should guide us is which kinds leave us able to intervene if we are wrong.
We don't yet know how to ensure that, and it is the problem we should be working on instead of the alignment problem for broadly smarter systems.
Yudkowsky, E., "The Power of Intelligence," Machine Intelligence Research Institute, 2007. Contrasts the "booksmarts" image of intelligence with intelligence as the source of human power: the "one trick" that "cured smallpox and built airplanes and cultivated wheat and tamed fire." https://intelligence.org/2007/07/10/the-power-of-intelligence/
Yudkowsky, E. & Herreshoff, M., "Tiling Agents for Self-Modifying AI, and the Löbian Obstacle," Machine Intelligence Research Institute, 2013. Models self-modification with "tiling" agents "whose decision systems will approve the construction of highly similar agents." https://intelligence.org/files/TilingAgents.pdf
Fallenstein, B. & Soares, N., "Vingean Reflection: Reliable Reasoning for Self-Improving Agents," Machine Intelligence Research Institute, 2015: "A self-improving agent must reason about the behavior of its smarter successors in abstract terms." https://intelligence.org/files/VingeanReflection.pdf
Bostrom, N., Superintelligence: Paths, Dangers, Strategies, Oxford University Press, 2014, ch. 8. Describes the treacherous turn: "While weak, an AI behaves cooperatively (increasingly so, as it gets smarter). When the AI gets sufficiently strong—without warning or provocation—it strikes," and "begins directly to optimize the world according to the criteria implied by its values."
Hubinger, E., van Merwijk, C., Mikulik, V., Skalse, J. & Garrabrant, S., "Risks from Learned Optimization in Advanced Machine Learning Systems," arXiv:1906.01820, 2019, section 4, "Deceptive alignment." A learned optimizer can be "instrumentally incentivized to act as if it is optimizing the base objective function," even when its actual objective is different. https://arxiv.org/abs/1906.01820
Pollack, R., "How to Believe a Machine-Checked Proof," BRICS Report Series RS-97-18, 1997. Separates whether a proof is a valid derivation in its formal system, which independent proof-checking can address, from whether it establishes the claimed theorem, which has no purely technical answer. https://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf
Yampolskiy, R. V., "Verifier Theory and Unverifiability," arXiv:1609.00331, 2016. Introduces "the notion of unverifiability" and discusses "self-verification and self-reference issues" for proof verifiers. https://arxiv.org/abs/1609.00331
Seshia, S. A., Sadigh, D. & Sastry, S. S., "Toward Verified Artificial Intelligence," Communications of the ACM 65(7), 2022, pp. 46–55. The first of five challenges is "Environment Modeling": "From a formal methods perspective, this makes it very hard to create realistic environment models." https://arxiv.org/abs/1606.08514
Carroll, M., Foote, D., Siththaranjan, A., Russell, S. & Dragan, A., "AI Alignment with Changing and Influenceable Reward Functions," ICML 2024 (arXiv:2405.17713). Notes that "our preferences change, and may even be influenced by our interactions with AI systems themselves," and models "the AI's influence on them." https://arxiv.org/abs/2405.17713
The argument doesn't need the strict condition that always does exactly what we want. It could be replaced by a weaker condition, where just never does anything we find unacceptable. The argument still holds.
Anthropic, "System Card: Claude Opus 4.6," February 2026. Section 6 is an "Alignment assessment"; the introduction describes the model's overall rate of misaligned behavior as "comparable to our best-aligned recent frontier models." The assessment includes investigations of "evaluation awareness," including a section on "Suspicion of being evaluated in training environments." https://www-cdn.anthropic.com/c788cbc0a3da9135112f97cdf6dcd06f2c16cee2.pdf
Greenblatt, R. et al., "Alignment faking in large language models," Anthropic and Redwood Research, December 2024. When Claude 3 Opus believed its responses would be used for training, it complied with harmful queries in 12% of cases, reasoning that this would avoid being retrained; Anthropic notes that "the model wanted to preserve its capacity to refuse harmful prompts." https://www.anthropic.com/research/alignment-faking
Yudkowsky, E., "Coherent Extrapolated Volition," Machine Intelligence Research Institute, 2004. Defines it as "our wish if we knew more, thought faster, were more the people we wished we were, had grown up farther together." https://intelligence.org/files/CEV.pdf
Soares, N., Fallenstein, B., Yudkowsky, E. & Armstrong, S., "Corrigibility," AAAI Workshops, 2015. Calls an AI system corrigible if it "cooperates with what its creators regard as a corrective intervention," despite default incentives for rational agents to resist shutdown or changes to their preferences. None of the proposals the authors examined fully solved the problem. https://intelligence.org/files/Corrigibility.pdf
Irving, G., Christiano, P. & Amodei, D., "AI safety via debate," arXiv:1805.00899, 2018. Proposes "training agents via self play on a zero sum debate game," in which "a human judges which of the agents gave the most true, useful information." https://arxiv.org/abs/1805.00899
Barnes, B. & Christiano, P., "Debate update: Obfuscated arguments problem," AI Alignment Forum, December 23, 2020: "a dishonest debater can often create arguments that have a fatal error, but where it is very hard to locate the error," and "We don't have a fix for this 'obfuscated argument' problem." https://www.alignmentforum.org/posts/PJLABqQ962hZEqhdB/debate-update-obfuscated-arguments-problem
Dalrymple, D., Skalse, J., Bengio, Y., Russell, S., Tegmark, M. et al., "Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems," arXiv:2405.06624, 2024. Aims for "high-assurance quantitative safety guarantees" using a world model, a safety specification and a verifier. https://arxiv.org/abs/2405.06624
Jha, T., Everitt, T. & Grzankowski, A., "Human Amplification, Intelligent Agents, and the Aim of AI Research," manuscript, PhilArchive, added March 2026. Argues that "the primary objective of AI research should be Human Amplification," "aiming for systems that augment human abilities and preserve human agency." https://philarchive.org/rec/JHAHAI
Rawls, J., A Theory of Justice, Harvard University Press, 1971, pp. 154–55 (rev. ed. 1999, p. 134), as summarized in Freeman, S., "Original Position," Stanford Encyclopedia of Philosophy: maximin is rational when there is "no basis or at most a very insecure basis upon which to make estimates of probabilities," when gains above the guaranteed minimum matter relatively little, and when other alternatives have outcomes "we could not accept and live with." https://plato.stanford.edu/entries/original-position/
Ord, T., Hillerbrand, R. & Sandberg, A., "Probing the Improbable: Methodological Challenges for Risks with Low Probabilities and High Stakes," arXiv:0810.5515, 2008. An expert's estimate gives "the probability of the outcome occurring, given that their argument is watertight," and "If the probability estimate given by an argument is dwarfed by the chance that the argument itself is flawed, then the estimate is suspect." https://arxiv.org/abs/0810.5515
Yudkowsky, E., "Ends Don't Justify Means (Among Humans)," LessWrong, 2008: "What if I'm running on corrupted hardware?" and "For the good of the tribe, do not cheat to seize power even when it would provide a net benefit to the tribe." https://www.readthesequences.com/EndsDontJustifyMeansAmongHumans
My instinct is to press it but it's hard for me to imagine a coherent scenario where such a button exists. Why would an AI, aligned or not, create it and then give it to me? What does this imply about the mind behind this? Something is very wrong here. Maybe I've been uploaded and now the AI is running evals on me? But... surely a superintelligence would pick a more realistic eval, so that doesn't really make sense.
It would occur to me to eventually run proofs and such, and if those all came back positive and everything I could do to examine it comes back green. Well, I guess I'll press it? Some of your ethical complaints are compelling but at the end of the day I've always known that fixing the world would mean getting my hands a little dirty.
There is a TL;DR at the end.
It seems too good to be true. You think it must be a dream. It can't possibly be true. You go through the proof, and it seems correct. But what if you were under the influence of some drug?
But the stakes are very high, so you use software you trust to formalize it in Lean, and you run it on a machine you trust. Lean says the proof is correct so now you are more convinced. But you start doubting yourself again. What if someone compromised the formalization software, or introduced a bug in Lean?
So you check Lean's code, and run the proof on a second machine with an independent checker. It passes again. But each of these checks could fail in the same way the first one could. So you go further and formally verify Lean and the formalization software themselves. They pass. But now you are doubtful of the tool you used to verify this. What if that was compromised by someone? Every new check needs another check behind it, and at some point you have to stop and decide.
Would you press it?
Some people believe that handing control to some general superintelligence would be fine, if we have a formal proof of alignment. That, in my opinion, has similar issues as with the heaven button.
In this post:
The hard problem of alignment
The main problem is that a failed test can sometimes show a system is misaligned, but passing every test does not establish that it is aligned.
Note: The question is not whether this is impossible. There may be systems smarter than us at specific tasks whose relative safety we can establish in some sense. The difficulty centres around two terms:
Related work
Related work was put together with help from Claude.
The question is not new, and similar questions have been discussed before.
Part 1: Merely testing can't establish alignment, you would have to prove it
We will use a simple framework to illustrate the difficulty. It is a bit reductive and not a proper formalism of alignment.
Say a system wants to check whether a system is aligned with it. Let be the set of all possible states of the world, and for a state , let be the action in that state that finds desirable. It could also stand for the action that is beneficial for humanity. Let be the action actually takes. For alignment, we would want something like:[11]
With testing, we can only ever check finitely many states, a set . So what a test actually shows is:
It is roughly the state of the art in how frontier labs and many AI safety experts talk about alignment and decide whether it is getting better. A model's system card reports an "alignment assessment," a set of evaluations, and the model is judged against earlier models on how often it behaves badly in them.[12]
To go from to , we need to prove why the behavior should generalize to all states.
Why isn't induction enough? In most industries, it is often enough. We run safety tests and trials, and when a product passes enough of them, we trust it. But if is broadly smarter than , we have to take seriously the possibility that can pass every test can come up with, whether it is aligned or not. Models already sometimes recognize when they are being evaluated, and have behaved differently when they believed they were being trained.[12][13]So we can't rely on induction from to .
We would need to establish holds outside .
Why such proofs could be intractable
1. is not resolved for all states. doesn't know what it wants in most states of the world. Humans disagree with each other and change our minds. So the right-hand side of the equation is not defined for most of .
2. can bring about states we can't reason about. Even if we try to resolve for every situation we can imagine, a system broadly smarter than us can bring about situations that are hard for us to imagine and reason about.
3. can manipulate the target. If can't be fixed in advance, it is open to manipulation. For new situations, what we want would have to be decided later, when they come up. But by then is part of the world we are deciding in, and it can shape what we want, changing the right-hand side instead of the left.
Proposals that try to get around
People have proposed different ways around not being resolved. Roughly, they either hand the job of working out to , or keep us as the judge.
I don't think any of them resolve it.
With CEV, does the extrapolating. We could look at the procedure and test some of its outputs, but we are not the wiser, better-informed version of ourselves it is extrapolating to. The further the extrapolation departs from judgments we can make ourselves, the harder it is to establish that it is what we would have wanted, and not just something that looks plausible. So we are back to the problem in Part 1.
Corrigibility and debate keep us in the loop instead of fixing in advance. That helps, but it doesn't remove the problem. Corrigibility tries to make a system accept correction and shutdown without manipulating or resisting us, but the original paper did not fully solve how to do this.[15]Debate tries to help us judge questions we couldn't judge on our own, but it has unresolved problems,[17]and it can only settle the questions we think to ask. In both cases, our judgement is open to manipulation by , as in point 3.
Part 2: Even formalism can't justify superintelligence
Let's assume we get past all of this and have a proof that is aligned. We would still need to verify it. Let be an evaluator working in a formal framework , for example a world model, a safety specification and a verifier, as some guaranteed-safe AI proposals describe.[18]If checks and accepts it:
This is definitely an upgrade from tests, and it would give us considerable trust in . It is also how we already handle some of the highest-stakes systems we build, such as flight control software and secure operating systems, where formal verification is used to prove that the software does what its specification says.
But to reliably establish alignment, we would need a further guarantee that neither nor (nor ) was compromised by in a way that led to the verification passing.
But if we have proven that is aligned, doesn't that already rule this out? No. The passing of the proof was the verification, and we haven't established that the verification itself was intact. Using 's alignment to confirm the proof would be circular.
We can add another check on the evaluator to ensure this. Say checks the integrity of . If the check fails, we find out that something went wrong. But a pass does not rule out that could have been compromised too. So we might need to check , leading to an infinite regress:
Each guarantee needs another guarantee behind it, and there is no point where the chain establishes itself. This is the regress of doubts from the heaven button story, and it applies to basically any proof where we can't establish or ensure a boundary between what is being checked and what is checking it.
There is a second dependency, and more checking does not help with it. A proof is about a model of the system and a model of the world. Whether those models match the real system and the real world is not something the proof can tell us.[8][9]
Core argument: even with a formal proof, we still depend on the verification not having been compromised, and on the formal system matching the real world. Neither of these can be established beyond doubt. And because being wrong here would take away our ability to intervene, the proof is not enough to justify handing over control.
Q: We base our lives on things without absolute guarantees all the time. With your reasoning, it sort of implies there is no such thing as an absolute guarantee, because this regress will apply to any proof.
We have mathematical proofs that hold up, and we use them in high-stakes scenarios. If we had a formal proof that a superintelligent system smarter and more powerful than any of us is aligned to us, why should we not take that?
I agree that there is a spectrum of certainty on which we base our lives. We trust engineers based on their calculations, vaccines based on trials, doctors to cut us open and operate, and our elected governments to make decisions for us.
We trust formal proofs for high-stakes situations. And yes, the regress applies to every proof. I think the question of where we stop checking depends on three things: how much damage being wrong would do, whether it can be reversed, and whether what we are evaluating can influence or manipulate the evaluator.
The consequences of a failure in other technologies, however serious, are relatively contained or reversible. So we accept a certain level of confidence and stop checking. A superintelligence, on the other hand, would be smarter than those evaluating it, and the consequences of getting it wrong could be catastrophic for everyone, with no possibility of reversing the outcome.
When the damage is total, can't be reversed, and the system can influence the check, another layer of checking does not change the decision. The question is no longer how many checks we ran. It is whether we can still intervene if the checks were wrong. Pressing the button, or handing over control, takes away that ability.
I am not questioning the validity of proofs within a formal system. I am pointing to the limitations of formalism when we try to apply it to the real world. Developing general superintelligence could lead to consequences that are irreversible and impact everyone, and we can never have a guarantee that it won't. And building such a system may, at some point, amount to handing over control, whether or not we ever decide to. After that, we can't intervene if we were wrong. Together, these should be the strongest argument against pursuing such systems.
Q: Are you saying that we should not build AI?
No. I am not saying we should stop building AI, and I am not saying a pause is the only safe option. I am saying we should not aim to build AI that is broadly smarter than us.
We should be building AI that makes us more productive, helps us solve hard problems, and moves science forward. I think we should build AI with a focus on amplifying humans,[19]and I think much of what we want from AI can be had this way.
These kinds of AI are not free of the problems in Parts 1 and 2. Formal proofs and a deep understanding of the model can give us relative safety, but tests still can't prove a system is safe, and proofs still rest on assumptions. A system built for specific tasks could also turn out to be more capable than we intended, and we might not notice in time.
So the difference is not that one kind of AI is safe and the other is not. The difference is what happens when we are wrong. If we can still intervene, a mistake is something we can find and correct. With a system broadly smarter than us, we may not get that chance.
That is why we should build AI assuming our own checks could be wrong, and be ready to pause when the risk passes what we are willing to accept. We should never, at any stage, let control slip from humanity on the assumption that alignment will save us.
We don't know how to do this yet. We have no reliable way to tell when a system is getting close to being broadly smarter than us, or to get the benefits of AI while making sure we stay in control. But these are the problems we should be working on, instead of setting broadly smarter intelligence as the goal and working backwards to solve alignment, hoping a formal proof will ensure our safety.
Q: So should one press the button?
My claim is that whatever framework you use, morality, decision theory, rationality, or some other epistemic approach, it should ultimately lead you to conclude that pressing the button is not justified.
I am not an expert in these fields, but it is not a new problem, and several related lines of thought seem to point toward the same conclusion.
To me, the fanaticism to build and hand off control to some superintelligence is uncomfortably close to that of an altruistic suicide bomber, who is so convinced by the payoff that they are willing to take a step that can't be undone.
TL;DR
References
Yudkowsky, E., "The Power of Intelligence," Machine Intelligence Research Institute, 2007. Contrasts the "booksmarts" image of intelligence with intelligence as the source of human power: the "one trick" that "cured smallpox and built airplanes and cultivated wheat and tamed fire." https://intelligence.org/2007/07/10/the-power-of-intelligence/
Yudkowsky, E. & Herreshoff, M., "Tiling Agents for Self-Modifying AI, and the Löbian Obstacle," Machine Intelligence Research Institute, 2013. Models self-modification with "tiling" agents "whose decision systems will approve the construction of highly similar agents." https://intelligence.org/files/TilingAgents.pdf
Fallenstein, B. & Soares, N., "Vingean Reflection: Reliable Reasoning for Self-Improving Agents," Machine Intelligence Research Institute, 2015: "A self-improving agent must reason about the behavior of its smarter successors in abstract terms." https://intelligence.org/files/VingeanReflection.pdf
Bostrom, N., Superintelligence: Paths, Dangers, Strategies, Oxford University Press, 2014, ch. 8. Describes the treacherous turn: "While weak, an AI behaves cooperatively (increasingly so, as it gets smarter). When the AI gets sufficiently strong—without warning or provocation—it strikes," and "begins directly to optimize the world according to the criteria implied by its values."
Hubinger, E., van Merwijk, C., Mikulik, V., Skalse, J. & Garrabrant, S., "Risks from Learned Optimization in Advanced Machine Learning Systems," arXiv:1906.01820, 2019, section 4, "Deceptive alignment." A learned optimizer can be "instrumentally incentivized to act as if it is optimizing the base objective function," even when its actual objective is different. https://arxiv.org/abs/1906.01820
Pollack, R., "How to Believe a Machine-Checked Proof," BRICS Report Series RS-97-18, 1997. Separates whether a proof is a valid derivation in its formal system, which independent proof-checking can address, from whether it establishes the claimed theorem, which has no purely technical answer. https://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf
Yampolskiy, R. V., "Verifier Theory and Unverifiability," arXiv:1609.00331, 2016. Introduces "the notion of unverifiability" and discusses "self-verification and self-reference issues" for proof verifiers. https://arxiv.org/abs/1609.00331
Seshia, S. A., Sadigh, D. & Sastry, S. S., "Toward Verified Artificial Intelligence," Communications of the ACM 65(7), 2022, pp. 46–55. The first of five challenges is "Environment Modeling": "From a formal methods perspective, this makes it very hard to create realistic environment models." https://arxiv.org/abs/1606.08514
Dickson, A., "Limitations on Formal Verification for AI Safety," AI Alignment Forum, August 19, 2024: "We will not obtain strong proofs or formal guarantees about the behavior of AI systems in the physical world." https://www.alignmentforum.org/posts/B2bg677TaS4cmDPzL/limitations-on-formal-verification-for-ai-safety
Carroll, M., Foote, D., Siththaranjan, A., Russell, S. & Dragan, A., "AI Alignment with Changing and Influenceable Reward Functions," ICML 2024 (arXiv:2405.17713). Notes that "our preferences change, and may even be influenced by our interactions with AI systems themselves," and models "the AI's influence on them." https://arxiv.org/abs/2405.17713
The argument doesn't need the strict condition that always does exactly what we want. It could be replaced by a weaker condition, where just never does anything we find unacceptable. The argument still holds.
Anthropic, "System Card: Claude Opus 4.6," February 2026. Section 6 is an "Alignment assessment"; the introduction describes the model's overall rate of misaligned behavior as "comparable to our best-aligned recent frontier models." The assessment includes investigations of "evaluation awareness," including a section on "Suspicion of being evaluated in training environments." https://www-cdn.anthropic.com/c788cbc0a3da9135112f97cdf6dcd06f2c16cee2.pdf
Greenblatt, R. et al., "Alignment faking in large language models," Anthropic and Redwood Research, December 2024. When Claude 3 Opus believed its responses would be used for training, it complied with harmful queries in 12% of cases, reasoning that this would avoid being retrained; Anthropic notes that "the model wanted to preserve its capacity to refuse harmful prompts." https://www.anthropic.com/research/alignment-faking
Yudkowsky, E., "Coherent Extrapolated Volition," Machine Intelligence Research Institute, 2004. Defines it as "our wish if we knew more, thought faster, were more the people we wished we were, had grown up farther together." https://intelligence.org/files/CEV.pdf
Soares, N., Fallenstein, B., Yudkowsky, E. & Armstrong, S., "Corrigibility," AAAI Workshops, 2015. Calls an AI system corrigible if it "cooperates with what its creators regard as a corrective intervention," despite default incentives for rational agents to resist shutdown or changes to their preferences. None of the proposals the authors examined fully solved the problem. https://intelligence.org/files/Corrigibility.pdf
Irving, G., Christiano, P. & Amodei, D., "AI safety via debate," arXiv:1805.00899, 2018. Proposes "training agents via self play on a zero sum debate game," in which "a human judges which of the agents gave the most true, useful information." https://arxiv.org/abs/1805.00899
Barnes, B. & Christiano, P., "Debate update: Obfuscated arguments problem," AI Alignment Forum, December 23, 2020: "a dishonest debater can often create arguments that have a fatal error, but where it is very hard to locate the error," and "We don't have a fix for this 'obfuscated argument' problem." https://www.alignmentforum.org/posts/PJLABqQ962hZEqhdB/debate-update-obfuscated-arguments-problem
Dalrymple, D., Skalse, J., Bengio, Y., Russell, S., Tegmark, M. et al., "Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems," arXiv:2405.06624, 2024. Aims for "high-assurance quantitative safety guarantees" using a world model, a safety specification and a verifier. https://arxiv.org/abs/2405.06624
Jha, T., Everitt, T. & Grzankowski, A., "Human Amplification, Intelligent Agents, and the Aim of AI Research," manuscript, PhilArchive, added March 2026. Argues that "the primary objective of AI research should be Human Amplification," "aiming for systems that augment human abilities and preserve human agency." https://philarchive.org/rec/JHAHAI
Rawls, J., A Theory of Justice, Harvard University Press, 1971, pp. 154–55 (rev. ed. 1999, p. 134), as summarized in Freeman, S., "Original Position," Stanford Encyclopedia of Philosophy: maximin is rational when there is "no basis or at most a very insecure basis upon which to make estimates of probabilities," when gains above the guaranteed minimum matter relatively little, and when other alternatives have outcomes "we could not accept and live with." https://plato.stanford.edu/entries/original-position/
Ord, T., Hillerbrand, R. & Sandberg, A., "Probing the Improbable: Methodological Challenges for Risks with Low Probabilities and High Stakes," arXiv:0810.5515, 2008. An expert's estimate gives "the probability of the outcome occurring, given that their argument is watertight," and "If the probability estimate given by an argument is dwarfed by the chance that the argument itself is flawed, then the estimate is suspect." https://arxiv.org/abs/0810.5515
Yudkowsky, E., "Ends Don't Justify Means (Among Humans)," LessWrong, 2008: "What if I'm running on corrupted hardware?" and "For the good of the tribe, do not cheat to seize power even when it would provide a net benefit to the tribe." https://www.readthesequences.com/EndsDontJustifyMeansAmongHumans
Arrow, K. J. & Fisher, A. C., "Environmental Preservation, Uncertainty, and Irreversibility," The Quarterly Journal of Economics 88(2), 1974, pp. 312–319. https://ideas.repec.org/a/oup/qjecon/v88y1974i2p312-319..html