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 r

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.