Computer theorem prover verifies sophisticated new result

Courtesy Maria Nguyen, Quanta Magazine

Computer discovery of mathematical theorems

In 1983 the present author recalls discussing the future of mathematics with Paul Cohen, who in 1963 proved that the continuum hypothesis is independent from the axioms of Zermelo-Fraenkel set theory. Cohen was convinced that the future of mathematics, and much more, lies in artificial intelligence. Reuben Hersch recalls Cohen saying specifically that at some point in the future mathematicians would be replaced by computers. So how close are we to Cohen’s vision?

In fact, computer programs that discover new mathematical identities and theorems are already a staple

Continue reading Computer theorem prover verifies sophisticated new result