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?
A common belief in AI labs and AI safety is that handing control to some general superintelligence would be fine, if we have a formal proof of alignment. That, in my opinion, is saying yes to the same button, except there is no proof yet, only the hope of one.
In this post, I present what I think is the hard problem of alignment.
First, I illustrate why testing for alignment is not enough and a proof would be required.
Then I lay out why a proof could be intractable.
Finally, I argue that 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 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.
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.
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:
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.[2]
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.[2][3]So we can't rely on induction from to .
Such a proof could come from different places: formal methods, a deep understanding of how the system was trained, interpretability, and so on. 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.[4]
Corrigibility doesn't try to fix at all. It asks for a system that lets us correct it or shut it down.[5]
Debate has two systems argue and lets a human judge which one gave the most true and useful information.[6]
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.[5]Debate tries to help us judge questions we couldn't judge on our own, but it has unresolved problems,[7]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 a proof 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.[8]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.
So even with a formal proof, we still depend on the verification not having been compromised, and on the formal system matching the real world. If we can't establish either of these well enough, and being wrong could take away our ability to intervene, then 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 two things: the cost of being wrong, and whether there is reason to believe that 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.
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 superintelligence could lead to irreversible consequences, and we can never have a guarantee that it won't. That alone should be the strongest argument against pursuing it.
Q: Are you saying that we should not build AI?
No. 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,[9]and never, at any stage, let control slip from humanity on the assumption that alignment will save us.
We can have relative safety for systems that are better than us at specific tasks, which can be useful to humanity in many different domains. Formal proofs and deep understanding of the model can help us establish those claims. We might have to be careful about the boundary between evaluator and evaluatee.
But we would need to imagine a different way of developing AI rather than proceeding with the goal of developing broadly smarter intelligence and working backwards to solve alignment including hopes to find formal proofs of such. Such an approach is bad, as there will not be a complete guarantee that things won't go really bad for everyone.
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.[10]
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.[11]
Corrupted hardware. Yudkowsky argued that we should not seize power even when it seems to benefit everyone, because our own reasoning might be compromised.[12]
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. And even a formal proof does not provide an absolute guarantee, as it does not guarantee the integrity of the proof, verifier, specification, and their connection to the real world. If those assumptions cannot themselves be adequately established, and failure could mean an irreversible loss of human control, then even formal verification is not enough to justify handing control to a superintelligence.
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/
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
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?
A common belief in AI labs and AI safety is that handing control to some general superintelligence would be fine, if we have a formal proof of alignment. That, in my opinion, is saying yes to the same button, except there is no proof yet, only the hope of one.
In this post, I present what I think is the hard problem of alignment.
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 whose relative safety we can establish in some sense. The difficulty centres around two terms:
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
With testing, we can only ever check finitely many states, a set
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.[2]
To go from
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
Such a proof could come from different places: formal methods, a deep understanding of how the system was trained, interpretability, and so on. We would need to establish
Why such proofs could be intractable
1.
2.
3.
Proposals that try to get around
People have proposed different ways around
I don't think any of them resolve it.
With CEV,
Corrigibility and debate keep us in the loop instead of fixing
Part 2: Even a proof can't justify superintelligence
Let's assume we get past all of this and have a proof
This is definitely an upgrade from tests, and it would give us considerable trust in
But to reliably establish alignment, we would need a further guarantee that neither
But if we have proven that
We can add another check on the evaluator to ensure this. Say
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.
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 two things: the cost of being wrong, and whether there is reason to believe that 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.
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 superintelligence could lead to irreversible consequences, and we can never have a guarantee that it won't. That alone should be the strongest argument against pursuing it.
Q: Are you saying that we should not build AI?
No. 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,[9]and never, at any stage, let control slip from humanity on the assumption that alignment will save us.
We can have relative safety for systems that are better than us at specific tasks, which can be useful to humanity in many different domains. Formal proofs and deep understanding of the model can help us establish those claims. We might have to be careful about the boundary between evaluator and evaluatee.
But we would need to imagine a different way of developing AI rather than proceeding with the goal of developing broadly smarter intelligence and working backwards to solve alignment including hopes to find formal proofs of such. Such an approach is bad, as there will not be a complete guarantee that things won't go really bad for everyone.
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
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. And even a formal proof does not provide an absolute guarantee, as it does not guarantee the integrity of the proof, verifier, specification, and their connection to the real world. If those assumptions cannot themselves be adequately established, and failure could mean an irreversible loss of human control, then even formal verification is not enough to justify handing control to a superintelligence.
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/
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