I'm not a mathematician but I'm curious if open ai is using these models to intelligently brute force their way towards proofs. It seems that AI is not thinking deeply and understanding abstract concepts leading to breakthroughs but is essentially searching the space by trying superhuman amounts of combinations, using programs like proof assistants to lock in findings.

It seems to me similar to when I ask a model to optimize a program - it starts with a known list of optimizations and then get's going until the metrics drop.

I'd like to know from a mathematician's perspective what AI's contributions to math is like.