I have no doubt that we are not far away from winning an IMO gold medal with an AI algorithm. I am not so sure it will come from the lean-team though. There are

I have no doubt that we are not far away from winning an IMO gold medal with an AI algorithm. I am not so sure it will come from the lean-team though. There are more people working in the direction, with varying focus on the AI or the automated prover aspect of things. I have the suspicion that AI-mathematicians will be foremost AI, and only secondary theorem provers. This is because what is mentioned in the article, mathematicians first look for patterns in these questions, and then apply their toolset to them. Only the final step is what theorem provers are currently good in. But, only time will tell which team will make it first to the finish line.