AI Threatens Mathematics

By: Yilling Sun

AI bots are not just coming for everyday jobs; they are also taking over mathematics. In a way, the threatening is done on purpose. Mathematicians didn't want to ground mathematics anymore. They developed formal systems, which were precise symbolic representations. This decision allowed mathematics to translateinto computer code.

Jeremy Avigad is a logician at Carnegie Mellon University.

“Euclid famously starts with ‘definitions’ that are almost poetic,” Avigad said. “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.”

Akshay Venkatesh, a mathematician at the Institute for Advanced Study in Princeton, doesn’t use AI yet but likes to talk about it.

“I want my students to realize that the field they’re in is going to change a lot,” Venkatesh said. “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.”

Mathematicians started using AI proof assistants, but these proof assistants frequently complain that the reasoning and logic of the mathematician are not understandable. That’s why mathematicians call the proof assistant “proof whiners.”

AI bots are being coded to help with mathematics, but some, like the proof assistant, aren’t working like they’re supposed to. Many people are coding AI to be better at math.