Comment by md_rumpf

Well... How do humans synthesizs programs then? We don't do exponential search over some symbols. We "somehow know" which branches get us closer to a program and which don't. It's foolish to believe it is impossible to teach an AI to "somehow know" this, too. Also: For some reason the bar is always higher for AI. Next to no human code is verifiably correct. And the actually verified-to-be-correct code is an even smaller subset.