I'm going to reduce (or understand someone else's reduction of) the stable AI self-modification difficulty related to Löb's theorem. It's going to happen, because I refuse to lose. If anyone else would like to do some research, this comment lists some materials that presently seem useful.

• The slides for Eliezer's Singularity Summit talk are available here, reading which is considerably nicer than squinting at flv compression artifacts in the video for the talk, also available at the previous link. Also, a transcription of the video can be found here.

• On provability logic by Švejdar. A little introduction to provability logic. This and Eliezer's talk are at the top because they're reference material. Remaining links are organized by my reading priority:

• Explicit Provability and constructive semantics by Artemov

• On Explicit Reflection in Theorem Proving and Formal Verification by Artemov. What I've read of these papers captures my intuitions about provability, namely that having a proof "in hand" is very different from showing that one exists, and this can be used by a theory to reason about its proofs, or by a theorem prover to reason about self modifications. As Artemov says, "The above difficulties with reading S4-modality ◻F as ∃x Proof(x, y) are caused by the non-constructive character of the existential quantifier. In particular, in a given model of arithmetic an element that instantiates the existential quantifier over proofs may be nonstandard. In that case ∃x Proof(x, F) though true in the model, does not deliver a “real” PA-derivation".

I don't fully understand this difference between codings of proofs in the standard model vs a non-standard model of arithmetic (On which a little more here). So I also intend to read,

• Truth and provability by Jervell, which looks to contain a bit of model theory in the context of modal logic and provability.

• Metatheory and Reflection in Theorem Proving by Harrison. This paper was a very thorough review of reflection in theorem provers at the time it was published. The history of theorem provers in the first nine pages was a little hard to digest without knowing the field, but after that he starts presenting results.

• Explicit Proofs in Formal Provability Logic by Goris. More results on the kind of justification logic set out by Artemov. Might skip if the Artemov papers stop looking promising.

• A new perspective on the arithmetical completeness of GL by Henk. Might explain further the extent to which ∃xProof(x, F), the non constructive provability predicate, adequately represents provability.

• A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points by Yanofsky. Analyzes a bunch of mathematical results involving self reference and the limitations on the truth and provability predicates.

• Provability as a Modal Operator with the models of PA as the Worlds by Herreshoff. I just want to see what kind of analysis Marcello throws out, I don't expect to find a solution here.