Phil, you might already understand, but I was talking about formal proofs, so your main worry wouldn't be the AI failing, but the AI succeeding at the wrong thing. (I.e., your model's bad.) Is that what your concern is?

Yes. Also, the mapping from the world of the proof into reality may obliterate the proof.

Additionally, the entire approach is reminiscent of someone in 1800 who wants to import slaves to America saying, "How can I make sure these slaves won't overthrow their masters? I know - I'll spend years researching how to make REALLY STRONG leg irons, and how to mentally condition them to lack initiative." That approach was not a good long-term solution.