If you read the article you can tell that AI is not the goal, it is a byproduct of the goal. The goal is to have confidence in the correctness of mathematical results proved by other experts.

Also, there has _already_ been some success on using AI to find proofs in lean.