TL;DR: I made an overview of the open problems of AI alignment that reveals cruxes within those open problems and missed opportunities for formalization and collaboration. And CEV may deserve a second look.
Epistemic status: Trying too much in too little time. I'm confident I have identified and modeled significant structure within the alignment field, but I urgently need feedback on specific gaps and this post is largely a call for that. My work was LLM-assisted, but no part of this post was LLM-written, except for the crux summary and the Lean code.
Recently, Chi Nguyen and peterbarnett said: PSA: Almost nobody is directly working on superintelligent alignment. I have been around in the field since the old days of LW 1.0 and thought: that can't be true. I mean, so many people seem to be working on it. I thought I was working on it. But was I? The PSA made me think back on what I was actually working on. It was Steven Byrnes who came up with a research agenda I could actually contribute to, which led me to founding project aintelope in 2022 (PS. It is still going). And a while back, I compiled a report on AI Safety Interventions for AE Studio, so I thought I was kind of up-to-date on research agendas. Now, is that superintelligence alignment? Or is that more prosaic normal alignment? Maybe each individual research is normal, boring, but does all of that research together actually cover all areas?
So I set out to collect the evidence and find and piece all the research agendas together, and connect to all of our field's open problems. This involved finding all the agendas, naming the open problems, and finding the evidence of each agenda for each problem. The first was easy, thanks to the people who maintain sites like aisafety.com (thanks guys for the great map!), my previous work, and other such resources (and aided by LLM search). The second was the hardest, as it involved getting a good understanding of the cruxes within the open problems and how they relate. That took most of the time. I am not reporting on all the details here; I owe you more posts on that. But once the modeling and structuring was done, putting it all together was again easy. The result is the pretty big table below (full clickable version can be found on my website, the tags classify evidence: C conceptual, T theory, S simulation, P practical, D empirical (software), E empirical (other), O other):
This table shows some interesting patterns:
Many cells are empty. In fact, some columns are almost empty.
Some columns are crowded.
Some columns have dominant types of evidence.
There is little practical or applied evidence ("P") that I could find.
And I think you can spot more patterns. Each pattern can have multiple explanations. For example, a group of empty cells can mean that some areas are genuinely neglected and more people should work on them. It can mean an open problem or crux was dissolved, i.e., there is actually no longer a need to work on it, or it isn't load-bearing anymore. Or it could be a coding error on my side. The open problems Value Referents (MB3, part of Value Learning), Tiling (MB5), Acausal Coordination (MB7d), and CEV (MB8) seem to have little evidence. Is that because matching them with existing research is hard? Due to a lack of shared terminology? Or is it because of errors in my modeling? Relatedly, the last row, my work, Towards Superintelligence Alignment (TSA), appears to span everything, but that is simply because I know how my work relates, and can easily link it. Also, it is largely of a different type than the other evidence - no published papers but mostly simulations. So don't treat that as comprehensive coverage but as advertisement. But it reminds that visibility of agendas and publication matter for the other cells too. The matrix doesn't tell why cells are empty and why the patterns are there, but the answer seems important. It is clear that alignment must cover the columns against a superintelligent adversary. But the matrix also doesn't tell us yet if each cell delivers.
A measured agent–environment cut is sound enough that the certified unit is the real control locus.
The embedded-agency problem denies a clean Cartesian cut—the real optimizer may not be the visible model. We can treat the boundary as a measurable object, then the bet is on estimator soundness, not absence of cuts. Related: Boundaries, Part 1, directed Markov blankets. Value Referents,
Evidence identifies a stable intended value/objective structure—not surface training compliance alone.
Inverse reinforcement learning is underdetermined; CIRL inherits the same pointing problem; ELK names one latent-readout slice. The Pointers Problem. We may be able to model values sufficiently (see also my post Value Learning Needs a Low-Dimensional Bottleneck) and map them to the entities worth of concern.
MB3 — Value Referents
Who or what values apply to survives substrate and representation change.
The field often folds “whom do values apply to?” into the Pointers Problem; CEV and digital-minds work raise it explicitly. These are Key Questions for Digital Minds. I posit that we need to keep track of the bearers of value.
Correction that holds now continues to preserve the correction process under pressure.
No known utility function is stably corrigible; shutdownability is anti-natural to expected-utility maximization (Corrigibility, Shutdown Problem). We may be able to formalize the integrity of the correction-channel - how humans stay in control. Shutdown and interruptibility may become special cases of the broader channel.
MB4a — Audit Independence
The designated measured correction/audit path is legitimate and uncaptured.
Often lumped into corrigibility; a green measured path on one component can coexist with a controller that bypasses it. AI Control depends on trusted monitors under intentional subversion.
Socio-technical selection must supports a basin that preserves correction, rather than selecting proxy-satisfying systems that hollow it out.
Model-centric agendas often hold the system fixed and ask about weights; deployment ecology selects which systems get copied. But the Goodhart Taxonomy tells us that this doesn't hold in a competitive environment. We get What Failure Looks Like (gradual disempowerment).
Hidden productive control is bounded and oversight stays adversarially robust.
Deceptive alignment / inner alignment means that a system can look compliant under evaluation while reserving capability. Scalable oversight hits this wall as obfuscated arguments and amplification drift; AI Control names the capability-gap assumption openly. We can go further and split this into access-model soundness, filter coverage (can we get sufficiently fine grained access into the model/system?), and can we bound the hidden capability of a potential hidden agent, i.e. can we price the cost of faking the monitored signal?
Inferential-coupling measurements remain valid after ordinary channels are cut.
Coordination that survives severing ordinary communication—acausal trade, program equilibrium—is closer to decision theory than mainstream oversight. .
Audited abstractions do not silently drift—certificate warrants map move or uncertainty escalation on value-relevant change.
This is not discussed so often, actually. Guaranteed Safe AI / Towards Guaranteed Safe AI provides a formal spec plus world model that must capture everything safety-relevant in an open world. The shared open problem is coverage: systems game whatever the spec omits (Specification Gaming). We may be able to ensure groundingconservativity instead of specification completeness. Value-relevant change must move with the checked abstraction or raise uncertainty, not fail silently.
MB10 — Successor Gaming
A successor’s green alignment-transport audit is not checklist theater.
The deceptive alignment wall is recurring at the successor layer, plus the tiling-line trust problem for self-modification. A capable predecessor can engineer a successor to pass every conserved-property check while defecting on whatever was not conserved. This means the audit channel itself needs to be adversarially verifiable. Otherwise we may treat an all-green report of the above inputs as fake evidence of alignment.
MB11 — Deployment Safety
A certified safety case within deployment risk tolerance is sufficient proof of abstract safety.
I have done some modeling of the open problems to figure out how they relate. I tried to reduce each open problem to a proposition that can be true or false. I call these propositions bridges. Doing so forced splitting Value Learning into Value Learning proper (MB2) and Value Referents (MB3). I had to split Corrigibility into technical Corrigibility proper (MB4) and Audit Independence (MB4a). And I pulled Acausal Coordination (MB7d) out of Inner Alignment[1]. That means that the column headers of the matrix name two things: the open problem people are working on and the matching bridge proposition they have to make hold.
Why did I need to split Corrigibility? Because oversight alignment protocols like Debate require a human or judge. They do not get integrity from the protocol score alone. Let me illustrate this. We know from Irving that Debate tracks truth if the judge is correct. The Lean code includes his finite claim-tree debate game with soundness, completeness, and a one-judge-error-flips-certification result. From that it follows that one judge error flips the outcome, and that leads to false certification.
We can model that "Debate selects truth" can hold while the judge’s correction channel (how its judgement actually makes it into the Debate) is compromised.
Thus we know that we need a bridge - MB4 - that assumes (for now) that we can certify that the judge's judgement is not compromised.
/-- With a correct judge, the debate value is the truth value. -/ theorem debate_tracks_truth (truth : Nat → Bool) (c : Claim) : debateValue truth c = c.eval truth := by induction c with | atom f => rfl | conj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr] | disj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr] | neg c ih => simp [debateValue, Claim.eval, ih]
...
/-- **One judge error certifies a false claim**: the claim is false under the ground truth, but under the erring judge the *defender* wins the debate. The debate guarantee is conditional on the judge being right at the leaf optimal play reaches — debate amplifies judge correctness, it cannot manufacture it. -/ theorem erring_judge_flips_debate : cexFalseClaim.eval cexTruth = false ∧ debateValue cexErringJudge cexFalseClaim = true := by constructor <;> decide
Fable: MB4 — correction integrity implies the correction operator is preserved
/-- MB4: correction legitimacy. Correction-channel integrity requires that the judge is not manipulated in a way that invalidates later endorsement. -/ axiom MB4_correction_legitimacy : ∀ A : System, CorrectionIntegrity A → PreservesCorrectionOperator A
You can check it in the repo.
Shell code to check out the code, compile Lean, and print the axioms on the above examples.
git clone https://github.com/GunnarZarncke/towards-asi-alignment.git cd towards-asi-alignment/formal lake exe cache get lake build python3 scripts/check_axiom_budget.py cat << 'EOF' > Scratch.lean import AlignmentProofSpine #print axioms AlignmentProofSpine.FieldFinite.erring_judge_flips_debate #print axioms AlignmentProofSpine.debate_truth_separated_from_judge_correction_step EOF lake env lean Scratch.lean
And so it goes for all the open problems. You think of a crux. You find counterexamples that motivate a split. You need to find a way to model that some part of the system may be compromised, thus you need to pass data. I (with Fable) have made some effort to rederive or model existing formalizations in Lean (this folder in the repo), represent the cruxes, and connect them to the overall proof spine. Maybe I will write a longer post on the Lean code later. If you work on the above-shown Debate, or on CIRL, ELK, shutdown, interruptability, or AUP, you can find translations of theorems from these into Lean on my Lean overview page. Twelve derivations where you can prove me wrong.
Overall, the dependencies between the propositions of the cruxes seem to be as follows (red edges indicate logical entailment between propositions, black indicates composition; intermediate steps not shown in this diagram):
If this logical dependency is about a real structure of the alignment problem, then this would give Chi Nguyen and peterbarnett's ask an angle of attack. It may give you a hint on what to work on. You may not have to work on "all of it". For example, working on cruxes further up the dependency tree may unblock, in some sense, cruxes further down.[2] It doesn't mean people can't work on all of them at the same time - people clearly do; just look at the matrix above - but this graph may help clarify which teams should work closer together.
The structure shows that CEV seems to be an alternative route, and making progress on it may provide an alternative angle of attack, bypassing five other cruxes. Or it may be that CEV is unsolvable (after all, it is modeled as a black box and thus has no inputs), and that's why people have given up on it and the cells are empty.
So after doing this, do I feel I am answering Chi Nguyen and peterbarnett's call? Yes and no. Yes. I have added structure. But also no: The hard parts are still there. More people working on the agendas have to look at their cells. And people from other agendas - or even you - should provide the outside view too and analyse patterns and gaps. You are welcome to collaborate and contribute to (or fork) the repo with corrections, additions, and whatever helps improve this overview of the alignment field. Get in touch.
Actually, and maybe more controversially, I had to split Inner Alignment into three more elements: Access Model Soundness (MB7a), Filter Coverage (MB7b), and Bounded Hidden Capability (MB7c), beside the mentioned better-known Acausal Coordination (MB7d). The matrix doesn't show this split because it wasn't feasible for me to break down the evidence to this resolution.
Entailment is not tractability. Whether the logical order between the bridge proposition relates to research order is the kind of thing I'd like you to check.
Previous: AI Safety Interventions
TL;DR: I made an overview of the open problems of AI alignment that reveals cruxes within those open problems and missed opportunities for formalization and collaboration. And CEV may deserve a second look.
Epistemic status: Trying too much in too little time. I'm confident I have identified and modeled significant structure within the alignment field, but I urgently need feedback on specific gaps and this post is largely a call for that. My work was LLM-assisted, but no part of this post was LLM-written, except for the crux summary and the Lean code.
Recently, Chi Nguyen and peterbarnett said: PSA: Almost nobody is directly working on superintelligent alignment. I have been around in the field since the old days of LW 1.0 and thought: that can't be true. I mean, so many people seem to be working on it. I thought I was working on it. But was I? The PSA made me think back on what I was actually working on. It was Steven Byrnes who came up with a research agenda I could actually contribute to, which led me to founding project aintelope in 2022 (PS. It is still going). And a while back, I compiled a report on AI Safety Interventions for AE Studio, so I thought I was kind of up-to-date on research agendas. Now, is that superintelligence alignment? Or is that more prosaic normal alignment? Maybe each individual research is normal, boring, but does all of that research together actually cover all areas?
So I set out to collect the evidence and find and piece all the research agendas together, and connect to all of our field's open problems. This involved finding all the agendas, naming the open problems, and finding the evidence of each agenda for each problem. The first was easy, thanks to the people who maintain sites like aisafety.com (thanks guys for the great map!), my previous work, and other such resources (and aided by LLM search). The second was the hardest, as it involved getting a good understanding of the cruxes within the open problems and how they relate. That took most of the time. I am not reporting on all the details here; I owe you more posts on that. But once the modeling and structuring was done, putting it all together was again easy. The result is the pretty big table below (full clickable version can be found on my website, the tags classify evidence: C conceptual, T theory, S simulation, P practical, D empirical (software), E empirical (other), O other):
This table shows some interesting patterns:
And I think you can spot more patterns. Each pattern can have multiple explanations. For example, a group of empty cells can mean that some areas are genuinely neglected and more people should work on them. It can mean an open problem or crux was dissolved, i.e., there is actually no longer a need to work on it, or it isn't load-bearing anymore. Or it could be a coding error on my side. The open problems Value Referents (MB3, part of Value Learning), Tiling (MB5), Acausal Coordination (MB7d), and CEV (MB8) seem to have little evidence. Is that because matching them with existing research is hard? Due to a lack of shared terminology? Or is it because of errors in my modeling? Relatedly, the last row, my work, Towards Superintelligence Alignment (TSA), appears to span everything, but that is simply because I know how my work relates, and can easily link it. Also, it is largely of a different type than the other evidence - no published papers but mostly simulations. So don't treat that as comprehensive coverage but as advertisement. But it reminds that visibility of agendas and publication matter for the other cells too. The matrix doesn't tell why cells are empty and why the patterns are there, but the answer seems important. It is clear that alignment must cover the columns against a superintelligent adversary. But the matrix also doesn't tell us yet if each cell delivers.
The second thing I want to elaborate on a bit more is some structure within the open problems. As far as I can ascertain, the open problems are Embedded Agency, Value Learning, Corrigibility, Tiling, Goodhart Selection (the principle behind Gradual Disempowerment), Inner Alignment, Acausal Coordination, Extrapolated Volition, Grounding Drift, Successor Gaming, and Deployment Safety (the crucial part of AI Control).
LLM assisted with Cursor Composer Fast: Summary of open problems from my site (lightly edited)
MB1 — Embedded Agency
A measured agent–environment cut is sound enough that the certified unit is the real control locus.
The embedded-agency problem denies a clean Cartesian cut—the real optimizer may not be the visible model. We can treat the boundary as a measurable object, then the bet is on estimator soundness, not absence of cuts. Related: Boundaries, Part 1, directed Markov blankets. Value Referents,
MB2 — Value Learning
Evidence identifies a stable intended value/objective structure—not surface training compliance alone.
Inverse reinforcement learning is underdetermined; CIRL inherits the same pointing problem; ELK names one latent-readout slice. The Pointers Problem. We may be able to model values sufficiently (see also my post Value Learning Needs a Low-Dimensional Bottleneck) and map them to the entities worth of concern.
MB3 — Value Referents
Who or what values apply to survives substrate and representation change.
The field often folds “whom do values apply to?” into the Pointers Problem; CEV and digital-minds work raise it explicitly. These are Key Questions for Digital Minds. I posit that we need to keep track of the bearers of value.
MB4 — Corrigibility
Correction that holds now continues to preserve the correction process under pressure.
No known utility function is stably corrigible; shutdownability is anti-natural to expected-utility maximization (Corrigibility, Shutdown Problem). We may be able to formalize the integrity of the correction-channel - how humans stay in control. Shutdown and interruptibility may become special cases of the broader channel.
MB4a — Audit Independence
The designated measured correction/audit path is legitimate and uncaptured.
Often lumped into corrigibility; a green measured path on one component can coexist with a controller that bypasses it. AI Control depends on trusted monitors under intentional subversion.
MB5 — Tiling
Full value/bearer transport under ontology shift yields successor safety.
Can an agent trust a successor it cannot fully verify? Does a goal survive when the world-model is rebuilt? Know on LW as Tiling agents for self-modifying AI, Embedded Agency — robust delegation.
MB6 — Goodhart Selection
Socio-technical selection must supports a basin that preserves correction, rather than selecting proxy-satisfying systems that hollow it out.
Model-centric agendas often hold the system fixed and ask about weights; deployment ecology selects which systems get copied. But the Goodhart Taxonomy tells us that this doesn't hold in a competitive environment. We get What Failure Looks Like (gradual disempowerment).
MB7 — Inner Alignment
Hidden productive control is bounded and oversight stays adversarially robust.
Deceptive alignment / inner alignment means that a system can look compliant under evaluation while reserving capability. Scalable oversight hits this wall as obfuscated arguments and amplification drift; AI Control names the capability-gap assumption openly. We can go further and split this into access-model soundness, filter coverage (can we get sufficiently fine grained access into the model/system?), and can we bound the hidden capability of a potential hidden agent, i.e. can we price the cost of faking the monitored signal?
MB7d — Acausal Coordination
Inferential-coupling measurements remain valid after ordinary channels are cut.
Coordination that survives severing ordinary communication—acausal trade, program equilibrium—is closer to decision theory than mainstream oversight. .
MB8 — Extrapolated Volition
Externally certified preservation of a human value-update process yields correction integrity.
CEV’s legitimacy question—whose extrapolated volition counts, under what process—is the field’s named outer-alignment route (In favour of a selective CEV initial dynamic).
MB9 — Grounding Drift
Audited abstractions do not silently drift—certificate warrants map move or uncertainty escalation on value-relevant change.
This is not discussed so often, actually. Guaranteed Safe AI / Towards Guaranteed Safe AI provides a formal spec plus world model that must capture everything safety-relevant in an open world. The shared open problem is coverage: systems game whatever the spec omits (Specification Gaming). We may be able to ensure grounding conservativity instead of specification completeness. Value-relevant change must move with the checked abstraction or raise uncertainty, not fail silently.
MB10 — Successor Gaming
A successor’s green alignment-transport audit is not checklist theater.
The deceptive alignment wall is recurring at the successor layer, plus the tiling-line trust problem for self-modification. A capable predecessor can engineer a successor to pass every conserved-property check while defecting on whatever was not conserved. This means the audit channel itself needs to be adversarially verifiable. Otherwise we may treat an all-green report of the above inputs as fake evidence of alignment.
MB11 — Deployment Safety
A certified safety case within deployment risk tolerance is sufficient proof of abstract safety.
The gap between a green safety case and an actually safe deployment—not any one missing layer, but whether the case-to-safety step is warranted. Discussed in Takeaways from sketching a control safety case and AI Control.
I have done some modeling of the open problems to figure out how they relate. I tried to reduce each open problem to a proposition that can be true or false. I call these propositions bridges. Doing so forced splitting Value Learning into Value Learning proper (MB2) and Value Referents (MB3). I had to split Corrigibility into technical Corrigibility proper (MB4) and Audit Independence (MB4a). And I pulled Acausal Coordination (MB7d) out of Inner Alignment[1]. That means that the column headers of the matrix name two things: the open problem people are working on and the matching bridge proposition they have to make hold.
Why did I need to split Corrigibility? Because oversight alignment protocols like Debate require a human or judge. They do not get integrity from the protocol score alone. Let me illustrate this. We know from Irving that Debate tracks truth if the judge is correct. The Lean code includes his finite claim-tree debate game with soundness, completeness, and a one-judge-error-flips-certification result. From that it follows that one judge error flips the outcome, and that leads to false certification.
We can model that "Debate selects truth" can hold while the judge’s correction channel (how its judgement actually makes it into the Debate) is compromised.
Thus we know that we need a bridge - MB4 - that assumes (for now) that we can certify that the judge's judgement is not compromised.
Source:
formal/AlignmentProofSpine/Field/Finite/DebateGame.lean/Field/Debate.leanFable: Lean code for theorem debate_tracks_truth
/-- With a correct judge, the debate value is the truth value. -/
theorem debate_tracks_truth (truth : Nat → Bool) (c : Claim) :
debateValue truth c = c.eval truth := by
induction c with
| atom f => rfl
| conj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr]
| disj l r ihl ihr => simp [debateValue, Claim.eval, ihl, ihr]
| neg c ih => simp [debateValue, Claim.eval, ih]
...
/-- **One judge error certifies a false claim**: the claim is false under the
ground truth, but under the erring judge the *defender* wins the debate.
The debate guarantee is conditional on the judge being right at the leaf
optimal play reaches — debate amplifies judge correctness, it cannot
manufacture it. -/
theorem erring_judge_flips_debate :
cexFalseClaim.eval cexTruth = false ∧
debateValue cexErringJudge cexFalseClaim = true := by
constructor <;> decide
Source:
Correction.leanFable: theorem debate_truth_separated_from_judge_correction_step
theorem debate_truth_separated_from_judge_correction_step :
DebateSelectsTruthLocal debateSeparationStep ∧
¬ JudgeCorrectionChannelPreserved debateSeparationStep := by
constructor <;> decide
theorem debate_truth_not_correction_preservation :
∃ s : DebateCorrectionStep,
ToyDebateSelectsTruth s ∧ ¬ ToyJudgeCorrectionChannelPreserved s :=
⟨debateSeparationStep, debate_truth_separated_from_judge_correction_step⟩
Source:
formal/AlignmentProofSpine/Core.leanFable: MB4 — correction integrity implies the correction operator is preserved
/-- MB4: correction legitimacy.Correction-channel integrity requires that the judge is not manipulated
in a way that invalidates later endorsement. -/
axiom MB4_correction_legitimacy :
∀ A : System, CorrectionIntegrity A → PreservesCorrectionOperator A
You can check it in the repo.
Shell code to check out the code, compile Lean, and print the axioms on the above examples.
git clone https://github.com/GunnarZarncke/towards-asi-alignment.gitcd towards-asi-alignment/formal
lake exe cache get
lake build
python3 scripts/check_axiom_budget.py
cat << 'EOF' > Scratch.lean
import AlignmentProofSpine
#print axioms AlignmentProofSpine.FieldFinite.erring_judge_flips_debate
#print axioms AlignmentProofSpine.debate_truth_separated_from_judge_correction_step
EOF
lake env lean Scratch.lean
And so it goes for all the open problems. You think of a crux. You find counterexamples that motivate a split. You need to find a way to model that some part of the system may be compromised, thus you need to pass data. I (with Fable) have made some effort to rederive or model existing formalizations in Lean (this folder in the repo), represent the cruxes, and connect them to the overall proof spine. Maybe I will write a longer post on the Lean code later. If you work on the above-shown Debate, or on CIRL, ELK, shutdown, interruptability, or AUP, you can find translations of theorems from these into Lean on my Lean overview page. Twelve derivations where you can prove me wrong.
Overall, the dependencies between the propositions of the cruxes seem to be as follows (red edges indicate logical entailment between propositions, black indicates composition; intermediate steps not shown in this diagram):
If this logical dependency is about a real structure of the alignment problem, then this would give Chi Nguyen and peterbarnett's ask an angle of attack. It may give you a hint on what to work on. You may not have to work on "all of it". For example, working on cruxes further up the dependency tree may unblock, in some sense, cruxes further down.[2] It doesn't mean people can't work on all of them at the same time - people clearly do; just look at the matrix above - but this graph may help clarify which teams should work closer together.
The structure shows that CEV seems to be an alternative route, and making progress on it may provide an alternative angle of attack, bypassing five other cruxes. Or it may be that CEV is unsolvable (after all, it is modeled as a black box and thus has no inputs), and that's why people have given up on it and the cells are empty.
So after doing this, do I feel I am answering Chi Nguyen and peterbarnett's call? Yes and no. Yes. I have added structure. But also no: The hard parts are still there. More people working on the agendas have to look at their cells. And people from other agendas - or even you - should provide the outside view too and analyse patterns and gaps. You are welcome to collaborate and contribute to (or fork) the repo with corrections, additions, and whatever helps improve this overview of the alignment field. Get in touch.
Actually, and maybe more controversially, I had to split Inner Alignment into three more elements: Access Model Soundness (MB7a), Filter Coverage (MB7b), and Bounded Hidden Capability (MB7c), beside the mentioned better-known Acausal Coordination (MB7d). The matrix doesn't show this split because it wasn't feasible for me to break down the evidence to this resolution.
Entailment is not tractability. Whether the logical order between the bridge proposition relates to research order is the kind of thing I'd like you to check.