AI in mathematics is forcing big questions • Hacker News Board

Re: AI in mathematics is forcing big questions

#161

Post by simonh » Sat, Jun 27, 2026, 4:07 PM UTC

zmgsabst wrote: post #146

simonh wrote: post #143

Earlier quoted context omitted.

It’s not a matter of what we want or don’t want, or are fine with. The universe doesn’t owe us explanations. Of course I’d prefer to understand everything, or as much as possible, but we don’t always get what we want.

You didn’t respond to his point: In the 40k universe, modern humanity is below not just their peak of technological prowess, but even their peak of pre-AI prowess. Because they landed in a valley of superstition involving machines they do not understand — and have no way to rebuild towards their peak, without yet further losses by moving away from the magical machines. That has nothing to do with the universe at larg…

I’m familiar with 40K, I played Laserburn back in the 80s. I met Bryan Ansel before 40K existed.

The comment I replied to equivocated between absolute limits to comprehensibility to humans and sociologically constructed limits, implying that thinking there may be the former makes someone ‘fine with’ the latter. That’s nonsense.

Re: AI in mathematics is forcing big questions

#162

Post by christianbryant » Sat, Jun 27, 2026, 4:07 PM UTC

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

Re: AI in mathematics is forcing big questions

#163

Post by pfdietz » Sat, Jun 27, 2026, 4:07 PM UTC

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?

Re: AI in mathematics is forcing big questions

#164

Post by [deleted] » Sat, Jun 27, 2026, 4:13 PM UTC

lioeters wrote: post #150

PunchyHamster wrote: post #147

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

News at 5: Team of corporate mathematicians working for OpenAI rewrites the foundation of mathematics in a billion lines of vibe-coded theorems and proofs that are so complex it's impossible for humans to review or understand. Next generation of children don't need to learn math anymore, they just get a subscription to OpenMath™.

[deleted]

Re: AI in mathematics is forcing big questions

#165

Post by sdenton4 » Sat, Jun 27, 2026, 4:32 PM UTC

robrain wrote: post #106

sdenton4 wrote: post #80

Earlier quoted context omitted.

How many people drive cars without knowing how an engine works? Or make a phone call without knowing how voice compression for a cellular network does it's thing? Or eats food without knowing how it came together from the supply chain?

The mechanic who repairs the cars knows how the engine works. The telco that manages loads and allocates networks knows how voice compression works. The farmers and supermarkets know how the supply chain works. None of your questions show why mathematics should include blobs of incomprehensible gloop, where no mathematician, no logician, no philosopher, no man on the street can make sense of said gloop, or use it in…

Well, you said people can't use things they don't understand.

But I'll take your expanded statement, to include riding a horse, something even older than the engine. We don't understand fully how a horse works -- biology is still a matter of seeing fragments of the whole -- but people had no problem riding and breeding them before the invention of the car, and before the discovery of genetics.

Meanwhile, understanding the math of a thing -- like stock markets, or nuclear bombs -- does not prevent its use from going badly.

Math is useful and beautiful, and a helpful tool for expanding our understanding of the world, but it is not the whole of understanding, or the sole factor in successful application of science to the world .

Signed, a mathematician.

Re: AI in mathematics is forcing big questions

#166

Post by UltraSane » Sat, Jun 27, 2026, 4:37 PM UTC

skybrian wrote: post #35

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 a…

I don't quite understand the objection. The 200,000 line Lean proof can be used in other proofs without needing to understand it. This is the biggest advantage of formally verified proofs.

Re: AI in mathematics is forcing big questions

#167

Post by robrain » Sat, Jun 27, 2026, 4:53 PM UTC

sdenton4 wrote: post #165

robrain wrote: post #106

Earlier quoted context omitted.

The mechanic who repairs the cars knows how the engine works. The telco that manages loads and allocates networks knows how voice compression works. The farmers and supermarkets know how the supply chain works. None of your questions show why mathematics should include blobs of incomprehensible gloop, where no mathematician, no logician, no philosopher, no man on the street can make sense of said gloop, or use it in…

Well, you said people can't use things they don't understand. But I'll take your expanded statement, to include riding a horse, something even older than the engine. We don't understand fully how a horse works -- biology is still a matter of seeing fragments of the whole -- but people had no problem riding and breeding them before the invention of the car, and before the discovery of genetics. Meanwhile, understandin…

I said no such thing - the comment that you just replied to is the first thing I’ve said in this thread.

Re: AI in mathematics is forcing big questions

#168

Post by Diogenesian » Sat, Jun 27, 2026, 5:13 PM UTC

bckgrndrdtn wrote: post #153

Diogenesian wrote: post #118

Earlier quoted context omitted.

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct.…

> These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.

That's not what I mean. I am talking about quirks and bugs that really are pretty subtle, and which really might turn up in e.g. a verified systems programming context: https://github.com/James-Hanson/junk-theorems-in-lean/blob/m... (there is a proof of 0=1 at the end - it is easy to understand where it comes from, but low-level compiler stuff like this is always a possibility.)

LLM agents will a) discover dumb counterintuitive stuff like this and b) exploit it to satisfy the kernel with c) the questionable lines being buried behind millions of lines of math slop. Humans have to check this stuff.

Re: AI in mathematics is forcing big questions

#169

Post by mmooss » Sat, Jun 27, 2026, 5:27 PM UTC

nok22kon wrote: post #52

mmooss wrote: post #42

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 pract…

always has been the poor kid always had disadvantages, had to help the family, while the rich kid could focus on the math, and maybe get into a good math place with family help

What's always been true is change. We decide our future. Sickness has always been there, but that doesn't mean we can't have a enormous influence on our fates.

So much that has been true for millenia we've changed in the last century or three.

Re: AI in mathematics is forcing big questions

#170

Post by slopinthebag » Sat, Jun 27, 2026, 5:47 PM UTC

nok22kon wrote: post #49

slopinthebag wrote: post #44

Earlier quoted context omitted.

Reminds me of a quote from Tsoding > “Programming is understanding. If you don't understand what you are doing, you are not programming. You are generating text.” Perhaps a proof without understanding is just generating numbers.

programming is also solving problems in medicine they use all kinds of drugs which they don't really understand how they work. anesthetics is a great example

By necessity perhaps, but they are desperate to find out why they work so doctors can kill less people. Almost half a million people die each year from medical errors in the USA.

Now they have a valid excuse that the human body is incredibly complex and not yet understood. We don’t have that excuse, because we build all of our software from the ground up. If we don’t understand it, that is our fault.