Right, you should use Lean or Coq. They are cleaner mathematically, which means AI has a better chance with them. And you can have the AI write proofs about their correctness. The proof-checker can verify the proofs and give you more trust in the AI’s work.

This isn’t foolproof - you still have to understand what was proved. And it may take some work to understand the unproven parts of the code. But I believe this is the path forward.