I didn't mean to have the AI write the proof. On the contrary. Humans would be responsible for writing them, to ensure that the code generated by the AI meet certain constraints (safety for example).