> The invariant for `K+D` is the identity function. So if we had a `D` with holes, we could use a prover to verify the identity invariant and “solve for D” simultaneously.

This was pretty mind-blowing for me. (I haven't really looked into program synthesis so I may be slightly more susceptible ;) There was one part of it that seemed problematic from my (perhaps flawed) understanding, though.

So I guess the idea is we have K+D = I (and this is roughly equivalent to 'D(K(s)) = I(s)' where 's' is a string to compress), so if we come up with a proof of 'I'—which would be a path through theorem space starting from I'm not sure what axioms—and we know 'I' is equivalent to 'K+D', and we already know the value of 'K,' then the value of 'D' is implied.

My question is what is the equivalent here to the subtraction operation that would allow us to say D = I - K? It seems very surprising to me that K and D would be structured in such a way that their own proofs would necessarily have any relationship to the proof we derived for I, so that such a subtraction would work so cleanly...