I'm a math graduate student, but also have great interest in computer capabilities. Chess players once thought that a machine cannot beat the world's best chess players because they cannot plan like humans despite their calculational power. Nowadays, computers are consistently beating the world's best human chess players with their developed strategic power. So, will computers also one day possess the ingenuity to do math proofs? Is that technology being worked on right now?