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...

Someday, human mathematicians might end up doing proofs for proofs.

When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it.

In those cases, we usually write tests.

But when tests get too big, we end up writing tests for the tests.

Eventually, it feels like we're heading into an era of proofs for proofs.

For me, this problem usually unfolds like this:

1.I can't trust SDKs or Stack Overflow code.

2.So I write tests.

3.But I can't trust the tests either.

4.So I use test coverage, mutation testing, property testing, and fuzzing.

5.If that's still not enough, I add formal verification.

6.And then the problem becomes: can I trust the verifier?

That's how it ends up. Wouldn't human work shift toward verifying the verification systems themselves?

Beyond the technical aspects, this new technology also leads to fundamental social changes.

In particular, until now, mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system.

With the raise of strong AI tools, only scientists in rich countries with access to those tools might be able to advance faster on the most difficult problems like the millennium problems.

Mathematics might become like experimental sciences were you need to build expensive machines to make further progress, such as nuclear fusion.

Actually, even now, the strongest models in mathematics are only available to a few engineers and a few mathematicians selected by Openai and Google.

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."

The big question is: why is government (or society) funding mathematics? What justifies this use of resources?

If it's utility, then why doesn't AI deliver utility? Isn't this an argument for AI?

One can expand this to various kinds of utility. Is knowing mathematical statements are true useful? In the ability to produce proofs useful? Does being able to prove carry over to other kinds of reasoning? Is producing a cadre of math-capable people useful in wartime? Is national prestige of value? There's a pro-AI reading of all these.

It it's beauty not utility, then why isn't math funding over with art funding, along with hills covered with acres of fabric, motorized embalmed animal carcasses, and religious symbols in bottles of urine?

Reading the article from the perspective of a non-mathematician the line that rang true for me was "I realized they derived joy, satisfaction, and meaning from the long journey toward understanding." My eldest child loves math and her whole life has been chaos except when she is solving math problems. I see that human element in science and I know deep down we need that.

I've been in the software industry for 30 years and I understand that sentiment perfectly on a personal level. However, also having used ChatGPT for the first time this year to help solve a technical problem, I was surprised to learn that feeling didn't go away. In fact, it was because I leaned on my experience and technical understanding to get to the point where I realized I needed help that I decided to try a new tool. I didn't feel any shame or disappointment in myself, rather I felt excited to learn something new that came out of the solution. It sent me on a new path of learning.

Now, that was research and not implementation. While plenty of code options were presented by ChatGPT, I analyzed the solution and educated myself from it. My final fix looked very different from the proposal because I do things a certain way, based on experience and learning from my many mistakes. In this scenario I was the secondary verification. My peers the tertiary. AI made the proposal, humans did the verification and could not have done so without cumulative knowledge and experience.

I have to assume that all fields utilizing AI will remain as they have always been, human education and experience will come first no matter what the tools available, because we are the ones impacted by the data produced by AI. As many math-oriented commenters here have already noted, human verification is a necessity and to do that, you must understand the discipline within which the data is being produced.

Personally, the idea of reaching solutions in math and computing (for example) exponentially beyond human capacity is exciting; I want certain answers before I die! But it still must be human-verified and the solutions should be for humans, not for machines, and not for "time to market". Repositories full of unvetted AI-generated code is bad enough, but once you start engineering structures, spacecraft and medicine strictly with AI, well...

I'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do more of of the same.

It is precisely NOT about big questions but rather potentially covering and thus cornering away all the "small" questions.

PS: already argued for something similar in recent Ergos related work, see comment history.

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.

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...

I always struggled with my lack of intuition vs that of my peers that had had a more comprehensive ‘math upbringing’.

Is direct experience and struggle really the only driver for developing intuition?

>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?

Argument started when 4 colour map proof was machine assisted. So 1976. (Which the fine article says: I remember my dad being in this argument at the time from the comp. sci side, albiet as a mathematicianby training)

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?

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.

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.

Is the big quesition same as in other domains, "how to stop AI bros from flooding us from slop that is made only to prove AI can do it too?"

[dead]

[dead]

[dead]

[flagged]

[flagged]