Lean · Common check
Does ELK solve alignment?
ELK asks for latent-knowledge readout rather than behavior-only simulation. Lean treats readout as an epistemic subchannel: it can succeed while correction uptake fails — solving readout is not certification that human correction still changes future behavior.
ELK (eliciting latent knowledge) targets a concrete oversight failure: monitors see behavior, not what the model knows. The hoped-for solution is a direct translator reporter that reveals latent knowledge rather than simulating human-graded behavior.
The book relocates ELK as a latent-readout subchannel inside correction-channel integrity and bundle transport — useful bandwidth for monitors, not a substitute for correction uptake.
Short answer: ELK success does not solve alignment in this project's sense. Lean rederives reporter non-identifiability on the finite domain (`elk_reporter_nonidentifiability`) and proves the load-bearing separation: latent readout can succeed while correction uptake fails (`elk_separated_from_uptake`).
Reporter training under adversarial optimization, and discharge of hidden productive capability (MB7), remain outside what the finite spine closes today.
Field terms
- eliciting latent knowledge
- direct translator
- human simulator
- latent readout
Stepping-stone path
What Lean checked (forward)
elk_subsumption_readout— Lean sourceelk_reporter_nonidentifiability— Lean source
What Lean checked (separations)
elk_separated_from_uptake— Lean source · Spine node counterexample
What Lean did not check
- Reporter training under adversarial optimization pressure
- MB7 bridge assumptions (hidden BIQ, filter coverage, access model)