AI proof assistants are like "flying cars". It's such an obvious idea, but it doesn't make sense. In reality, writing math proofs is the absolute last thing that AI will be able to do.
There's a perception that "Machines are good at math therefore they should be good at proofs." Couldn't be farther from the truth.