AI in mathematics is forcing big questions

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use:

> A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs and abstractions, without which no autoformalization could take place. By contrast, Math Inc’s autoformalized proof of Viazovska’s results exposes no intelligible interface. Who in their right mind would merge a 200,000-line unaudited vibe-coded blob into the master branch of global human science?

https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...

The use of computers in mathematics has been somewhat controversial from the very start.

There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understanding. I like this one quote by (allegedly) Wigner that illustrates it well:

"It is nice to know that the computer understands the problem, but I would like to understand the problem, too."

I think we’re going to find out the hard way that the proofs left to solve are very much not elegant.

Human mathematicians could become “priests to oracles.”

Priests were interpreting the oracles (at least at a place like Delphi) according to the context of the people asking the questions aka participating in politics of that ancient times.

Subjectivity was a feature and I’m not sure that fits to mathematics though.

I wonder if mathematics as a science field moves more into engineering or if a different branch will emerge that is closer to that because to the point of the article, science is about understanding not just results.

>more recently, a new general-purpose AI system from OpenAI disproved an important conjecture in combinatorial geometry. This result would have been worthy of publication in a major mathematics journal if humans had been the authors

The quality of the mathematics is a function of who has authored it?

Turns out you have to be Terence Tao to know when an LLM is right or wrong

The article poses if AI will be a tool, a collaborator or an oracle. Why not all 3?

If mathematics is human understanding of logical consequences, understanding is the priority. But if AI proves something we can't understand but can utilize, that is a different sort of useful.

We are getting awfully close to "the answer of the universe is 42" and having it not be a joke...

Much can be resolved when it is understood math is discovered not created. AI is a tool. if it makes discovery or proof easier that is still mathematics. A proof stands on its own logic regardless how it is derived. The root concern is how ai may provide uplift for mathematical discovery outside of socially expected channels.

There's yet another major issue of the centralization of power and knowledge:

> Some worry about the accessibility of AI tools. Traditionally, mathematicians have required little more than intuition, training, and a pen and paper to advance their field. If this slow, deliberative process is no longer valued by society, and particularly by research funders, then mathematics could become an elitist activity, only practiced by select organizations that can afford to work with proprietary AI models.

This can be true of anything LLMs do better than existing options. Because the best LLMs require enormous resources to develop, access to them can be very limited. Right now they are priced for market share. What happens when your small law firm attorney, or self-representation, goes up against a large firm with LLM expertise? Can the kid from the poor high school compete with the kid from the rich school with premium LLM access, in mathematics for example?

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it.

It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify the correctness. One hallucination in 300 steps of logic is enough to destroy the entire proof.

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very expensive and propitiatory. They are not like the commercial AI that regular people use. It takes considerable prompting and trial an error to solve even Olympiad/Putnam problems, and tons of work by humans pouring over the results to see if it's correct. For every Erdos problem that captures the headlines, there are many where it failed or untold hours of prompting and token burn to get that result, and manhours verify it.

[dead]

[dead]

[dead]

[flagged]

[flagged]