AI tools are shaping next-generation theorem provers, and with them the relationship between math and machine. By Stephen Ornes.
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.
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.
Another gripe is that if they want to use theorem provers, mathematicians must first learn to code and then figure out how to express their problem in computer-friendly language.
Mathematicians, logicians and philosophers have long argued over what part of creating proofs is fundamentally human, and debates about mechanized mathematics continue today, especially in the deep valleys connecting computer science and pure mathematics.
“Computers have done amazing calculations for us, but they have never solved a hard problem on their own Until they do, mathematicians aren’t going to be buying into this stuff.”
– Kevin Buzzard, a mathematician at Imperial College London
Recently, Simon DeDeo together with Scott Viteri, a computer scientist now at Stanford University, reverse-engineered a handful of famous canonical proofs (including one from Euclid’s Elements) and dozens of machine-generated proofs, written using a theorem prover called Coq, to look for commonalities. Very interesting read!
[Read More]