My understanding is that relatively little success has been achieved in that direction. I'd love to be corrected if there's something I haven't learned of, but

My understanding is that relatively little success has been achieved in that direction. I'd love to be corrected if there's something I haven't learned of, but as far as I know no theorem of any significance has been independently originated and proven by a computer. Rather, computers are increasingly used to assist human mathematicians. Machine learning has recently been used to help with identifying and proving interesting theorems [1] but still very much as a tool for human mathematicians rather than an independent artificial mathematical "mind". Personally I think the ability to truly "do mathematics" may be a marker of AGI. If/when we have machines independently mapping out new and interesting areas of mathematics the way human mathematicians do I suspect we will have cracked meaning/understanding. FWIW I've felt that way for over thirty years and have never considered the Turing test a convincing marker of intelligence, so I don't consider myself to be moving goalposts when I find the (absolutely incredible) feats of the current generation of ML algorithms unconvincing as evidence that we're nearing AGI. [1] https://www.maths.ox.ac.uk/node/40529 https://www.maths.ox.ac.uk/node/40529