AI Helping Mathematicians

[Gord_in_Toronto]

Maths researchers hail breakthrough in applications of artificial intelligence

https://phys.org/news/2021-12-maths-hail-breakthrough-applications-artificial.html

For the first time, computer scientists and mathematicians have used artificial intelligence to help prove or suggest new mathematical theorems in the complex fields of knot theory and representation theory.

The astonishing results have been published today in the pre-eminent scientific journal, Nature.

(Emphasis mine.)

While computers have long been used to generate data for experimental mathematics, the task of identifying interesting patterns has relied mainly on the intuition of the mathematicians themselves.

That has now changed.

"We have demonstrated that, when guided by mathematical intuition, machine learning provides a powerful framework that can uncover interesting and provable conjectures in areas where a large amount of data is available, or where the objects are too large to study with classical methods."

Slowly. Slowly. The computers are taking over.

 

[hecd2]

Slowly. Slowly. The computers are taking over.

Perhaps. But a rather less breathless quote from the Nature paper itself:


"Rather than use machine learning to directly generate conjectures, we focus on helping guide the highly tuned intuition of expert mathematicians, yielding results that are both interesting and deep."

and

"There are limitations to where this framework will be useful—it requires the ability to generate large datasets of the representations of objects and for the patterns to be detectable in examples that are calculable."

But yeah, this is fascinating, and considering how far we've come with the application of computers in a relative blink of an eye,. who can say where we'll end up.

 

[sphenisc]

Perhaps. But a rather less breathless quote from the Nature paper itself:


"Rather than use machine learning to directly generate conjectures, we focus on helping guide the highly tuned intuition of expert mathematicians, yielding results that are both interesting and deep."

and

"There are limitations to where this framework will be useful—it requires the ability to generate large datasets of the representations of objects and for the patterns to be detectable in examples that are calculable."

But yeah, this is fascinating, and considering how far we've come with the application of computers in a relative blink of an eye,. who can say where we'll end up.

Call me when a computer can untangle its own cable.

 

[W.D.Clinger]

To wrap some context around this news, major microprocessor manufacturers have been using automatic theorem provers and automated proof assistants to prove correctness of their designs for several decades now, starting around 1995 when ACL2 was used to prove correctness of floating point division in the AMD K5 processor.

Way back in 1975, I worked as grader for a graduate course in automatic theorem proving taught by Woody Bledsoe. Bledsoe's graduate students included Bob Boyer, who developed the Boyer-Moore theorem prover with J Strother Moore, who leads the ongoing ACL2 project. In the meantime, several other important theorem provers and proof assistants have been developed and entered mainstream use.

The novelty claimed in the opening post of this thread has to do with suggesting and proving conjectures in two specific areas of mathematics: knot theory and representation theory. That "breakthrough" builds on a long history of applying similar technology to other areas of mathematics and computer science.