> Certainly such an AI would be able to just write machine code directly and verify it through whatever means, including formal proofs, as needed. Why does it need a compiler?

If the AI can write the program bytecode through AI magic, why can’t it verify that it works through AI magic?

The AI needs a compiler for the program for same reason it needs a proof language to verify it.