Feedback Loops Guide AI to Proof Checking

Some of the earliest work on artificial intelligence (AI) saw mathematics as a major target and key to making breakthroughs quickly. In 1961, leading computer scientist and AI pioneer John McCarthy argued at the Fifth Symposium in Pure Mathematics that the job of checking mathematical proofs would likely be "one of the most interesting and useful applications of automatic computers." McCarthy saw the possibility for mathematicians to try out different ideas for proofs quickly that the computers then tested for correctness. More than 60 years later, such a proof assistant has yet to appear. But recent developments in both mathematics and computer science may see a breakthrough sooner rather than later.