I've been thinking about this since AlphaDev, but the same sort of program that can build sorting algorithms can also prove math theorems using an automated pro

I've been thinking about this since AlphaDev, but the same sort of program that can build sorting algorithms can also prove math theorems using an automated proof checker. The real question is if it can be used to prove something significant, not just trivial findings.