Mathematical Beauty, Truth and Proof in the Age of AI

Arthur T Knackerbracket has processed the following story:

The best proofs are works of art. They're not just rigorous; they're elegant, creative and beautiful. This makes them feel like a distinctly human activity - our way of making sense of the world, of sharpening our minds, of testing the limits of thought itself.

But proofs are also inherently rational. And so it was only natural that when researchers started developing artificial intelligence in the mid-1950s, they hoped to automate theorem proving: to design computer programs capable of generating proofs of their own. They had some success. One of the earliest AI programs could output proofs of dozens of statements in mathematical logic. Other programs followed, coming up with ways to prove statements in geometry, calculus and other areas.

[...] They have not, as yet, built systems that can generate the proofs from start to finish, but that may be changing. In 2024, Google DeepMind announced that they had developed an AI system that scored a silver medal in the International Mathematical Olympiad, a prestigious proof-based exam for high school students. OpenAI's more generalized large language model," ChatGPT, has made significant headway on reproducing proofs and solving challenging problems, as have smaller-scale bespoke systems. It's stunning how much they're improving," said Andrew Granville, a mathematician at the University of Montreal who until recently doubted claims that this technology might soon have a real impact on theorem proving. They absolutely blow apart where I thought the limitations were. The cat's out of the bag."

Researchers predict they'll be able to start outsourcing more tedious sections of proofs to AI within the next few years. They're mixed on whether AI will ever be able to prove their most important conjectures entirely: Some are willing to entertain the notion, while others think there are insurmountable technological barriers. But it's no longer entirely out of the question that the more creative aspects of the mathematical enterprise might one day be automated.

Andrew Granville worries that outsourcing more rigorous aspects of mathematics to AI could adversely affect researchers' ability to think. I feel that my own understanding is not from the bigger picture," he said. It's from getting your hands dirty."

Even so, most mathematicians at the moment have their heads buried firmly in the sand," Granville said. They're ignoring the latest developments, preferring to spend their time and energy on their usual jobs.

[...] He and a relatively small group of other mathematicians are now starting to examine what an AI-powered mathematical future might look like, and how it will change what they value. In such a future, instead of spending most of their time proving theorems, mathematicians will play the role of critic, translator, conductor, experimentalist. Mathematics might draw closer to laboratory sciences, or even to the arts and humanities.

Read more of this story at SoylentNews.