Make way, mathematicians, here comes AlphaProof

At the headquarters of Google DeepMind, an artificial intelligence lab in London, researchers have a set ritual for announcing major results: They strike a large ceremonial gong.

In 2016, the gong sounded for AlphaGo, an AI system that excelled at the game of Go. In 2017, the gong sounded as AlphaZero conquered chess. On each occasion, the algorithm had defeated human world champions.

Last week, DeepMind researchers pulled out the gong again to celebrate what Alex Davies, a leader of Google DeepMind's mathematics initiative, described as a "huge breakthrough" in mathematical reasoning by an AI system. A pair of Google ...