Perhaps this is the wrong venue, but I'm curious how this work generalizes and either applies or doesn't apply to other lines of research.

Schmidhuber's group has several papers on "Goedel machines" and it seems like they involve the use of proofs to find self-rewrites.

We present the first class of mathematically rigorous, general, fully self-referential, self-improving, optimally efficient problem solvers. Inspired by Kurt Gödel's celebrated self-referential formulas (1931), a Gödel machine (or 'Goedel machine' but not 'Godel machine') rewrites any part of its own code as soon as it has found a proof that the rewrite is useful, where the problem-dependent utility function and the hardware and the entire initial code are described by axioms encoded in an initial proof searcher which is also part of the initial code.

Their 2005 paper "Completely Self-Referential Optimal Reinforcement Learners" explained the design and their 2012 paper "Towards an Actual Gödel Machine Implementation" seems to be working towards making something vaguely practical. This is the same group whose PhD students helped founded of DeepMind (like Shane Legg as founder and several others as very early employees). Deepmind was then acquired by Google in 2014.

Since that architecture uses a theorem proving system, and creates new versions of itself, and can even replace its own theorem proving system, it naively seems like the Löbstacle might come up. Are you familiar with Schmidhuber's group's work? Does it seem like their work will run into the Löbstacle and they're just not talking about it? Or does it seem like their architecture makes worries about the Löbstacle irrelevant via some clever architecting?

Basically, my question is "The Löbstacle and Gödel Machines... what's up with them?" :-)