When AI proves theorems, it uses divide-and-conquer approach just as humans - it breaks a big theorem into lemmas and tackles lemmas one by one.

An alternative approach where it is just one big-ass logical expression is just not better.

Same thing with code, I think - you need some intermediate results like a calling convention, helper subroutines, etc.

A sufficiently powerful AI can do compilation "mentally" - i.e. producing machine code conforming to a specific calling convention. It can also decompile machine code. But you, obviously, don't gain anything doing it this way, if there's one-to-one correspondence between high-level code and machine code. You might as well just write high-level code.

I really hope that software becomes more efficient. But I don't think that it can only be done by generating machine code directly.