Much has been said about superintelligences cooperating with each other via reasoning or proving statements about each other's source code. But it seems like this "source code" is likely to be a neural network rather than something amenable to formal methods, in which case it's not at all clear that the problem is computationally tractable. If this has been discussed before, can someone point me to the discussion?