Comment by tarsierscripter | Hacker News Reader

Comment by tarsierscripter | Hacker News Reader

Parent Full thread

tarsierscripter

Sure, mathematics will survive and even prosper with AI, but what about the mathematicians

It's not a given that mathematics will survive without mathematicians. It's not even likely. The proofs OpenAI threw over the wall are unpublishable garbage, top to bottom. A big reason mathematicians are so upset is that they feel like they've been drafted into the role of unpaid editor for OpenAI.

Make no mistake about it, the mathematical profession is under attack. The biggest incentive for becoming a mathematician (as opposed to a hired gun quant) is the challenge of solving the proofs. Take that away and the most talented problem solvers go with it.

In time, the profession of mathematics will evolve so a new task is at the center of the diagram--maybe it will be explaining math results to humans or teaching math to future mathematicians.

That is the centre of mathematics. It's what schools pay mathematicians to do. All the research stuff, the problem solving, the "thrill of the hunt" for elusive proofs, and the prestige of being the first? That's the carrot the schools dangle in front of mathematicians' noses to get them to work. Without that, you don't get exceptional mathematicians teaching classes and supervising grad students (and attracting the world's top students to your school); you get adjuncts and only adjuncts.

I've seen two mathematicians (Dana Moshkovitz and David Harvey) state that the proofs were greek to them as written but that other models understood the papers just fine and could break it down and explain it to them.

Dana Moshkovitz: "Basically the paper is so horribly written that it’s impossible to read it without AI help. I asked Astra for reasonable completeness and soundness claims of the noise gadget and it gave them by combining claims from all over the paper."

David Harvey: "The bottom line is that I think the claimed result is plausible. I have not actually read the paper. In fact, there are three closely related papers [papers], and I have not read any of them. I tried, but soon gave up. The math(s) dump does not appear to be strong on exposition. Instead, I asked Fable to explain [paper] to me. Fable seems to understand the argument and thinks that it is correct. I expect that thousands of frontier LLM instances around the world have come to the same conclusion over the last two weeks. If not, surely we would have heard by now. At first I did not understand Fable’s explanations. But I asked questions, and then asked more questions, and drilled down towards the core of the problem. Gradually I started to understand parts of the argument. I have seen enough now to arrive at the tentative belief that the main result is possibly correct (notice that I choose my words very carefully), and that the bound O(n(log n) α) has the right shape. I stress that I have not checked the proof in any serious level of detail, and there are many parts that I do not yet understand properly. In the sections below I will try to explain what I have learned so far, and why I lean towards thinking it might be correct."

Without AI help? Impossible. With AI help? Comprehensible.

That is consistent with the assertion that mathematics might outlast human mathematicians.

(Feels related to models evolving forms of human-incomprehensible shorthand when communicating among themselves.)

This is similar to some of the software being produced these days, where it's impossible to understand or develop the codebase further without AI. The complexity is beyond what even an above average individual human brain can comprehend.

Without making a value judgement of whether that's good or bad for the field in the long term, it is an interesting point to note the similarity with the human-incomprehensible communication among AI agents. When there are no humans in the loop, it's no longer necessary to translate or "lower" the representation for our benefit.

Since it's still early days, we can only imagine and extrapolate how far it might go in that direction, what might evolve out of it in the future. There could be entire fields of research that AI agents are busy working on and pushing forward, that humans can barely understand, if at all.

This is where we at my workplace. Up and down the chain nobody really understands the code anymore, it's obvious when you ask specific questions about it. Everyone is using Ai to generate, review, and ask questions of the code, but nobody has a good intuition of what's going on anymore.

Dana Moshkovitz is a computer scientist, not a pure mathematician. The work she does may have practical applications even if the proofs may be incomprehensible, just as incomprehensible software can still be useful.

Incomprehensible pure mathematics has no value to anyone.

If those OpenAI proofs are unpublishable garbage then our concept of publishing has to change. Pure math will probably shift from journals publishing PDFs to individuals (or their agents) posting Lean code in Git repos.

That’s of no use to anyone. Haven’t you been following this story? The value of a pure math proof is the understanding it brings and the additional questions raised along the way. Its truth value is of minor consequence.

That’s like skipping to the end of an important novel and thinking you got something out of it.

I've been following the story. Git repos of Lean code are a good start to developing understanding. First verify that the proof is correct, then work on ways to simplify it and make it understandable.

Many of the proofs released by Open AI don’t have Lean proofs. Their system doesn’t work in Lean directly, it writes proofs in natural language first. Later, some of the proofs were passed through an auto-formalization model to generate Lean code which then passed Lean’s checks.

The issue is that the auto-formalization step itself is not trivial. There is no formal verification which proves the translation correct, so it is up to mathematicians to hand-check the formalization to make sure it’s saying the same thing. Unfortunately, this problem is undecidable in general.

We’ve already had a paper showing that auto-formalization can’t be trusted implicitly [1], so a GitHub repo of a bunch of Lean code can’t be trusted to prove what the title claims is being proved.

[1] https://arxiv.org/abs/2610.08144

> That’s like skipping to the end of an important novel and thinking you got something out of it.

Wasn't it just a few years ago that there were all sorts of apps ("Blinkist" ?) being pushed hard that did just that: give you the TLDR on some publication so that you could pretend to have read & understood it?

If Astra manages to genocide journal publishing I'd instantly consider it the crowning achievement of tech

Many journals already have a no AI policy no?

Reply on news.ycombinator.com