[doriantaylor]

FYI I've already gotten some feedback re the (human attention and computational) cost of proof systems. I'm not sure yet if this problem is (exactly) the same as that.