Automated Math Reasoning

In our earliest AI courses,we learned about theorem proving using AI. And yes, it was not automated math reasoning.  But it gave you the hope that it could be done, if only you could state the problem at hand as purely mathematical.   Or even parts of it.  But it was never so.  Like the article says, it rarely intersects exactly with the real world, except for elements of the real world that are also approximations within contexts.  Bottom line, its still hard.    Good article explains it, with hopes for the next generation.

How Close Are Computers to Automating Mathematical Reasoning? in Quanta Mag.  Stephen Ornes
Contributing Writer 

AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine.

n the 1970s, the late mathematician Paul Cohen, the only person to ever win a Fields Medal for work in mathematical logic, reportedly made a sweeping prediction that continues to excite and irritate mathematicians — that “at some unspecified future time, mathematicians would be replaced by computers.” Cohen, legendary for his daring methods in set theory, predicted that all of mathematics could be automated, including the writing of proofs.

A proof is a step-by-step logical argument that verifies the truth of a conjecture, or a mathematical proposition. (Once it’s proved, a conjecture becomes a theorem.) It both establishes the validity of a statement and explains why it’s true. A proof is strange, though. It’s abstract and untethered to material experience. “They’re this crazy contact between an imaginary, nonphysical world and biologically evolved creatures,” said the cognitive scientist Simon DeDeo of Carnegie Mellon University, who studies mathematical certainty by analyzing the structure of proofs. “We did not evolve to do this.”

Computers are useful for big calculations, but proofs require something different. Conjectures arise from inductive reasoning — a kind of intuition about an interesting problem — and proofs generally follow deductive, step-by-step logic. They often require complicated creative thinking as well as the more laborious work of filling in the gaps, and machines can’t achieve this combination.

Computerized theorem provers can be broken down into two categories. Automated theorem provers, or ATPs, typically use brute-force methods to crunch through big calculations. Interactive theorem provers, or ITPs, act as proof assistants that can verify the accuracy of an argument and check existing proofs for errors. But these two strategies, even when combined (as is the case with newer theorem provers), don’t add up to automated reasoning.  .... "