.jpg)
.jpg)
AI is coming for mathematics, too
New York Times
- +
- -
In the collection of the Getty Museum in Los Angeles is a portrait
from the 17th century of the ancient Greek mathematician Euclid: disheveled,
holding up sheets of “Elements,” his treatise on geometry, with grimy hands.اضافة اعلان
For more than 2,000 years, Euclid’s text was the paradigm of mathematical argumentation and reasoning. “Euclid famously starts with ‘definitions’ that are almost poetic,” Jeremy Avigad, a logician at Carnegie Mellon University, said in an email. “He then built the mathematics of the time on top of that, proving things in such a way that each successive step ‘clearly follows’ from previous ones, using the basic notions, definitions, and prior theorems.” There were complaints that some of Euclid’s “obvious” steps were less than obvious, Avigad said, yet the system worked.
But by the 20th century, mathematicians were no longer willing to ground mathematics in this intuitive geometric foundation. Instead, they developed formal systems — precise symbolic representations, mechanical rules.
Eventually, this formalization allowed mathematics to be translated into computer code. In 1976, the four-color theorem — which states that four colors are sufficient to fill a map so that no two adjacent regions are the same color — became the first major theorem proved with the help of computational brute force.
The latest transformative force
Now mathematicians are grappling with the latest transformative force: artificial intelligence.
In 2019, Christian Szegedy, a computer scientist formerly at Google and now at a startup in the Bay Area, predicted that a computer system would match or exceed the problem-solving ability of the best human mathematicians within a decade. Last year he revised the target date to 2026.
Akshay Venkatesh, a mathematician at the Institute for Advanced Study in Princeton and a winner of the Fields Medal in 2018, is not currently interested in using AI, but he is keen on talking about it. “I want my students to realize that the field they’re in is going to change a lot,” he said in an interview last year. He recently added by email: “I am not opposed to thoughtful and deliberate use of technology to support our human understanding. But I strongly believe that mindfulness about the way we use it is essential.”
In February, Avigad attended a workshop about “machine-assisted proofs” at the Institute for Pure and Applied Mathematics, on the UCLA campus. (He visited the Euclid portrait on the final day of the workshop.) The gathering drew an atypical mix of mathematicians and computer scientists. “It feels consequential,” said Terence Tao, a mathematician at the university, winner of a Fields Medal in 2006 and the workshop’s lead organizer.
Tao noted that only in the past couple of years have mathematicians started worrying about AI’s potential threats, whether to mathematical aesthetics or to themselves. That prominent community members are now broaching the issues and exploring the potential “kind of breaks the taboo,” he said.
Students work on a group project during the Formalization of Mathematics summer school at the Simons Laufer Mathematical Sciences Institute in Berkeley, Calif. on June 14, 2023. For thousands of years, mathematicians have adapted to the latest advances in logic and reasoning. Are they ready for artificial intelligence?
One conspicuous workshop attendee sat in the front row: a trapezoidal box named “raise-hand robot” that emitted a mechanical murmur and lifted its hand whenever an online participant had a question. “It helps if robots are cute and nonthreatening,” Tao said.
Bring on the ‘Proof Whiners’
These days there is no shortage of gadgetry for optimizing our lives — diet, sleep, exercise. “We like to attach stuff to ourselves to make it a little easier to get things right,” Jordan Ellenberg, a mathematician at the University of Wisconsin-Madison, said during a workshop break. AI gadgetry might do the same for mathematics, he added: “It’s very clear that the question is, what can machines do for us, not what will machines do to us.”
One math gadget is called a proof assistant, or interactive theorem prover. (“Automath” was an early incarnation in the 1960s.) Step-by-step, a mathematician translates a proof into code; then a software program checks whether the reasoning is correct. Verifications accumulate in a library, a dynamic canonical reference that others can consult.
This type of formalization provides a foundation for mathematics today, said Avigad, the director of the Hoskinson Center for Formal Mathematics (funded by crypto entrepreneur Charles Hoskinson), “in just the same way that Euclid was trying to codify and provide a foundation for the mathematics of his time.”
Of late, the open-source proof assistant system Lean is attracting attention. Developed at Microsoft by Leonardo de Moura, a computer scientist now with Amazon, Lean uses automated reasoning, which is powered by what is known as good old-fashioned artificial intelligence, or GOFAI — symbolic AI, inspired by logic. So far, the Lean community has verified an intriguing theorem about turning a sphere inside out as well as a pivotal theorem in a scheme for unifying mathematical realms, among other gambits.
But a proof assistant also has drawbacks: It often complains that it does not understand the definitions, axioms, or reasoning steps entered by the mathematician, and for this it has been called a “proof whiner.” All that whining can make research cumbersome.
But Heather Macbeth, a mathematician at Fordham University, said that this same feature — providing line-by-line feedback — also makes the systems useful for teaching.
In the spring, Macbeth designed a “bilingual” course: She translated every problem presented on the blackboard into Lean code in the lecture notes, and students submitted solutions to homework problems both in Lean and prose. “It gave them confidence,” Macbeth said, because they received instant feedback on when the proof was finished and whether each step along the way was right or wrong.
Since attending the workshop, Emily Riehl, a mathematician at Johns Hopkins University, used an experimental proof-assistant program to formalize proofs she had previously published with a co-author. By the end of a verification, she said, “I’m really, really deep into understanding the proof, way deeper than I’ve ever understood before. I’m thinking so clearly that I can explain it to a really dumb computer.”
Read more Technology
Jordan News
For more than 2,000 years, Euclid’s text was the paradigm of mathematical argumentation and reasoning. “Euclid famously starts with ‘definitions’ that are almost poetic,” Jeremy Avigad, a logician at Carnegie Mellon University, said in an email. “He then built the mathematics of the time on top of that, proving things in such a way that each successive step ‘clearly follows’ from previous ones, using the basic notions, definitions, and prior theorems.” There were complaints that some of Euclid’s “obvious” steps were less than obvious, Avigad said, yet the system worked.
But by the 20th century, mathematicians were no longer willing to ground mathematics in this intuitive geometric foundation. Instead, they developed formal systems — precise symbolic representations, mechanical rules.
Eventually, this formalization allowed mathematics to be translated into computer code. In 1976, the four-color theorem — which states that four colors are sufficient to fill a map so that no two adjacent regions are the same color — became the first major theorem proved with the help of computational brute force.
The latest transformative force
Now mathematicians are grappling with the latest transformative force: artificial intelligence.
In 2019, Christian Szegedy, a computer scientist formerly at Google and now at a startup in the Bay Area, predicted that a computer system would match or exceed the problem-solving ability of the best human mathematicians within a decade. Last year he revised the target date to 2026.
Akshay Venkatesh, a mathematician at the Institute for Advanced Study in Princeton and a winner of the Fields Medal in 2018, is not currently interested in using AI, but he is keen on talking about it. “I want my students to realize that the field they’re in is going to change a lot,” he said in an interview last year. He recently added by email: “I am not opposed to thoughtful and deliberate use of technology to support our human understanding. But I strongly believe that mindfulness about the way we use it is essential.”
In February, Avigad attended a workshop about “machine-assisted proofs” at the Institute for Pure and Applied Mathematics, on the UCLA campus. (He visited the Euclid portrait on the final day of the workshop.) The gathering drew an atypical mix of mathematicians and computer scientists. “It feels consequential,” said Terence Tao, a mathematician at the university, winner of a Fields Medal in 2006 and the workshop’s lead organizer.
Tao noted that only in the past couple of years have mathematicians started worrying about AI’s potential threats, whether to mathematical aesthetics or to themselves. That prominent community members are now broaching the issues and exploring the potential “kind of breaks the taboo,” he said.
Students work on a group project during the Formalization of Mathematics summer school at the Simons Laufer Mathematical Sciences Institute in Berkeley, Calif. on June 14, 2023. For thousands of years, mathematicians have adapted to the latest advances in logic and reasoning. Are they ready for artificial intelligence?
One conspicuous workshop attendee sat in the front row: a trapezoidal box named “raise-hand robot” that emitted a mechanical murmur and lifted its hand whenever an online participant had a question. “It helps if robots are cute and nonthreatening,” Tao said.
Bring on the ‘Proof Whiners’
These days there is no shortage of gadgetry for optimizing our lives — diet, sleep, exercise. “We like to attach stuff to ourselves to make it a little easier to get things right,” Jordan Ellenberg, a mathematician at the University of Wisconsin-Madison, said during a workshop break. AI gadgetry might do the same for mathematics, he added: “It’s very clear that the question is, what can machines do for us, not what will machines do to us.”
One math gadget is called a proof assistant, or interactive theorem prover. (“Automath” was an early incarnation in the 1960s.) Step-by-step, a mathematician translates a proof into code; then a software program checks whether the reasoning is correct. Verifications accumulate in a library, a dynamic canonical reference that others can consult.
This type of formalization provides a foundation for mathematics today, said Avigad, the director of the Hoskinson Center for Formal Mathematics (funded by crypto entrepreneur Charles Hoskinson), “in just the same way that Euclid was trying to codify and provide a foundation for the mathematics of his time.”
Of late, the open-source proof assistant system Lean is attracting attention. Developed at Microsoft by Leonardo de Moura, a computer scientist now with Amazon, Lean uses automated reasoning, which is powered by what is known as good old-fashioned artificial intelligence, or GOFAI — symbolic AI, inspired by logic. So far, the Lean community has verified an intriguing theorem about turning a sphere inside out as well as a pivotal theorem in a scheme for unifying mathematical realms, among other gambits.
But a proof assistant also has drawbacks: It often complains that it does not understand the definitions, axioms, or reasoning steps entered by the mathematician, and for this it has been called a “proof whiner.” All that whining can make research cumbersome.
But Heather Macbeth, a mathematician at Fordham University, said that this same feature — providing line-by-line feedback — also makes the systems useful for teaching.
In the spring, Macbeth designed a “bilingual” course: She translated every problem presented on the blackboard into Lean code in the lecture notes, and students submitted solutions to homework problems both in Lean and prose. “It gave them confidence,” Macbeth said, because they received instant feedback on when the proof was finished and whether each step along the way was right or wrong.
Since attending the workshop, Emily Riehl, a mathematician at Johns Hopkins University, used an experimental proof-assistant program to formalize proofs she had previously published with a co-author. By the end of a verification, she said, “I’m really, really deep into understanding the proof, way deeper than I’ve ever understood before. I’m thinking so clearly that I can explain it to a really dumb computer.”
Read more Technology
Jordan News
NEWS RELATED TO