Hacker News Reader

Comment by TheOtherHobbes | Hacker News Reader

Math proofs need to produce the correct output correctly, which is not quite the same thing.

This looks like an AI IPO PR powerplay, because at this point the proofs haven't been checked and it may not be possible for a human to check them - because proofs should be clear, not horribly written and noisy.

The noise is suspicious because it's the difference between brute forcing and cognition. A human proof won't just be logically correct, it will be cognitively distilled and coherent. It may still take years to understand it, but the logical flow will be straightforward, not obfuscated.

You want the path through the maze to be as short as possible and the map to be as clear as possible.

This sounds like the opposite. There may be a genuine path through the maze, but if it's too convoluted and takes too long it will be impossible to confirm.

I think the next step is to demand that proofs either be human-scale or they prove that a human-scale proof is impossible and the machine proof is as good as it gets.

I suspect that's possible without tripping over the halting problem. (But I can't prove it.)

View on HN

That reminds me of this paper:

Chow, T. Y. (2008). A beginner’s guide to forcing (arXiv:0712.1320). arXiv. https://doi.org/10.48550/arXiv.0712.1320

> “All mathematicians are familiar with the concept of an open research problem. I propose the less familiar concept of an open exposition problem. Solving an open exposition problem means explaining a mathematical subject in a way that renders it totally perspicuous. Every step should be motivated and clear; ideally, students should feel that they could have arrived at the results themselves. The proofs should be “natural” in Donald Newman’s sense [13]:

> This term . . . is introduced to mean not having any ad hoc constructions or brilliancies. A “natural” proof, then, is one which proves itself, one available to the “common mathematician in the streets.””

This, but for a generalised notion of "number" (that is, "proof")

https://en.wikipedia.org/wiki/Nothing-up-my-sleeve_number

> I think the next step is to demand that proofs either be human-scale or they prove that a human-scale proof is impossible and the machine proof is as good as it gets.

In 1976, the proof of the Four Color Theorem was controversial because it was done with a computer examining over 1000 cases by brute force and was essentially not comprehensible by humans. But mathematicians ended up accepting it. So mathematics has a 50-year precedent of not requiring human-scale proofs. How is the current situation different?

(Disclaimer: Apologies if this sounds dismissive or argumentative. I genuinely think that the Four Color Theorem should play a role in these discussions and suspect that many people are unaware of the controversy over it.)

There's also another (that I find more concerning) aspect to it.

As AIs become smarter and smarter, there will be no amount of clarity that will make more complex proofs understandable to humans - this is an inevitable effect of the cognitive capacity gap.

Complaining about bad style can make some sense now (I disagree anyway), but it's an argument that will be dead shortly.

Arguably no human understands 100% of how a smartphone is produced, and, it doesn't matter?

Maybe no human will fully understand a future proof, but they could fully understand a little piece of it. And many humans in aggregate could understand it, each with their own little piece.

The point isn't that 1 person can understand an entire smartphone silicon up. It's that 100% of a smartphone can be understood by people. A maths theorem that can only be partially understood/proven only has value as marketing collateral.

>A maths theorem that can only be partially understood/proven only has value as marketing collateral.

There are many problems that aren't "interesting" in a mathematical sense but can still have valuable proofs. The entire field of formal methods in software development is mostly about this kind of problem. If I want to be sure that no input can cause out-of-bounds memory access, or that my superoptimizer found the lowest possible cycle count, I don't care if it's elegant, I just need some machine-readable proof I can run through my trusted verifier.

When we use verification to build software. We have an actual software as an output and hopefully some sort of problem solvsd the verification is also not in an of itself valuable.

The verification itself is valuable because it gives us confidence that the software is correct. This knowledge changes what we do with the software. E.g. do we need to sandbox it before processing untrusted inputs? Is it safe to put it on a hostile network? Can we use it to control an airplane or a nuclear reactor? Even if the code remains identical, formally verifying software improves it because it lets us use it in situations where unverified software would be too risky.

For one person that understands a proof of some matrix multiplication algorithm lowering its current complexity bound in an useful way (e.g. not with absurdly gigantic <= 2nd order polynomial term), there's likely thousands of companies willing to pay for the improved efficiency

And if anything that useful does come out of this output/"slop dump" then that might begin to make a strong argument for it. But every other time it was "that's the theorem done for the headline figuring out everything important and how to use it is an exercise for the reader".

> A maths theorem that can only be partially understood/proven only has value as marketing collateral.

If this is true, then what's really the point of math? A lot of math is actually useful. A proof regarding cryptography, for example, would have practical application even if not understandable by humans.

Cryptography is 100% understandable by humans so I'm not sure what the point is. You do understand that the argument isn't everything has to be understandable by every human right just to check?

While any logical proof written in lean can be broken down into things a human can follow, there is no requirement that the whole proof of something is ever simple enough that all humans combined could follow it.

Given the LLMs are struggling to explain themselves clearly, but also that these explanations cleared up somewhat by having an expert using one to query some of this research, but also the LLMs can solve problems faster than humans can read the proofs, it is possible for this category to have both examples of things that can be rendered in a human-comprehensible form, and also examples where it is not.

As an analogy: any human can check any single arithmetical calculation from a computer, that's not even particularly difficult. But a Raspberry Pi Zero can do those arithmetical calculations so fast that even if literally every single human was trained to do this at the level of the current world record holder, humanity as a whole could not keep up.

Exactly. We need "observability tools" that allow us to keep a handle on things we can't see or comprehend innately.

We have such tools for a large number of events that we're incapable of witnessing or understanding in "raw form".

We can't possibly read through thousands of raw records of recordings of individual's heights and make sense of it. But we can use Excel to calculate the average in seconds. We can chart the results and the image is perfectly comprehensible. We can trust the average calculation and the image because we trust the mechanism for transforming the data. We have what I would call a trusted path of provenance. We don't need to nor do we want to read the raw data.

Now we need things like this of the 2nd order. We need mechanisms of transforming trusted paths of provenance into things we can look at and easily verify.

We can do formal verification of code that would be hard to do by hand. We need formal verification tools for formally verifying formal verification tools. Eventually we will need multiple layers of this. As long as the chain and reasoning is intact, we should be alright.

It's kind of like with a horse. A horse is much stronger than us, but we can control it by pulling on two strategically connected pieces of rope.

I don't know much about this controversy, but looking at the Wikipedia page for the Four Color Theorem, it looks like since the initial Appel-Haken result, mathematicians have continued to work on the Four Color Theorem to try to find a simpler proof. So did they really accept it?

Finding new simpler proofs happens in traditional manual mathematics too.

There are a lot of proofs for Pythagoras' Theorem and other theorems.

There are mappings between complex numbers and 2D matrices allowing problems to be solved in either domain.

There's research into The Langlands Program looking to connect number theory and harmonic analysis.

There's research into Category Theory looking to define core concepts and relate them do different fields so that results in one field can be applied to another due to equivalence.

Mathematicians (mostly) accepted that the proof was valid, not that it was the kind of thing mathematics should strive for.

If intelligence is compression, and these models are a different form of lesser intelligence than human, but being scaled up to brute force problems, then it makes sense the artifacts that produce (the proofs) would have worse compression than a human proof would.

In other domains I have seen first hand overwhelming evidence of how things that cause the AI to make mistakes also cause humans to make the same mistakes.

I wonder if the proofs being produced that are hard for humans to interpret are also hard for other LLMs to interpret.

In other words, I wonder if humans are still much better at compressing understanding into proofs than the best LLMs, and what it will take for LLMs to exceed them.

It kind of an explicit example of how the LLMs can be materially less intelligent than people, but still be more productive through scaling, and yet they also can't replace people because they are a categorically different kind of intelligence. It's like all the AI debates compressed into one example showing countwr-intuitive answers.

idk if i'd even say they're "lesser", just very different. so they look like gods/babies depending on what they're doing because we anthropomorphise them.

In terms of synapse density, neuron diversity, energy efficiency, memory access, etc. they are orders of magnitude lesser.

My mental model - for better or worse - is that intelligence has both shape and area, and LLMs are orders of magnitude smaller area but very different shape, and they have more intelligence area in the kind that humans have lesser of.

So yes very different, more in some material ways and lesser in others, but in total intelligence are still orders of magnitude lesser.

My gp comment was acknowledging that when you scale up many instances / brute force problems it confuses that "total area" claim a bit.

To follow the anthropomorphization... 1000 toddlers may have more total intelligence than a grown man, but does that matter?

The problem with these discussions probably/usually fold into differing/loose definitions of intelligence.

ok yeah then i think we're in total agreement

perhaps the chat-based ux has sort of fooled us into comparing these things to human intellegence. we don't really do this with chess, or other forms of ai, nor computers at large.

This is just the first cut. I have no doubt that they will polish their proofs over time.

I don't see how they have any incentive to do so.

I communicated loosely; I meant AI users in general, not OpenAI specifically.

My hunch is that improving those proofs specifically might be a similar endeavour as improving a large vibe coded app.

It's a search problem; finding the shortest and most elegant path through the space of arguments.

> I wonder if humans are still much better at compressing understanding into proofs than the best LLMs, and what it will take for LLMs to exceed them.

Isn't it fairly established that (generally [0]) manually written / optimized skill files perform a lot better than generated ones? Meaning that yes, this likely does hold.

[0] or to be specific, that the pecking order is: ai generated < human co/written < hyperoptimized for the specific model via some convergence process

> A human proof won't just be logically correct, it will be cognitively distilled and coherent. It may still take years to understand it, but the logical flow will be straightforward, not obfuscated.

https://en.wikipedia.org/wiki/Inter-universal_Teichmüller_th... seems like a counterpoint, but IANAM. (I am likely cherrypicking the far end of the bell curve re: straightforward here)

Isn't this controversial, to say the least?

Not a counterpoint, actually case in point, because:

>Mochizuki and a few other mathematicians claim that the theory indeed yields such a proof but this has so far not been accepted by the mathematical community.

Proof can't be understood, proof doesn't matter.

Oh the proof can be understood quite well: it is understood to be wrong.

I wait for AI to say something about this :)

Someone at OpenAI, please, work on this.

Funny enough.

There is ongoing AI assisted work on this, and precisely the problematic gap in the theory (around Corollary 3.12).

As of now, a required step appears to definitely be missing, but it's not clear if this is a genuine / unrepairable defect.

https://zen.ac.jp/news/zmcpostevent0331e

https://github.com/lana-agents/iut

https://github.com/LANA-Project/genl

> the difference between brute forcing and cognition

There’s not really a clear distinction between these things, in my opinion. Problem solving (and intelligence?) is a mix of search and compression. We like solutions that are elegant (high compression, simple search). But often what appears elegant to some is harder to appreciate for those without the same background knowledge or even the same amount of mental bandwidth (if you’ve ever worked with someone simply much, much smarter than you, you may intuit this!).

> The noise is suspicious because it's the difference between brute forcing and cognition. A human proof won't just be logically correct, it will be cognitively distilled and coherent. It may still take years to understand it, but the logical flow will be straightforward, not obfuscated.

This is basically how all AI approaches appear to work. They solve the problem you give them (in many cases) but in a very over-complicated way.

It's like they can't step back from the problem and realise that they need to simplify to make it work better. Nope, just keep hammering more code/proofs against the problem and eventually you'll hit the goal.

RL has a lot to answer for, I guess.

> It's like they can't step back from the problem and realise that they need to simplify to make it work better. Nope, just keep hammering more code/proofs against the problem and eventually you'll hit the goal.

There is nothing wrong with that approach if it accomplishes the goal faster, i.e. you can work at the speed of an AI.

The post says there's a Lean certificate for this and other proofs ("some [...] not all of them").

> This looks like an AI IPO PR powerplay,

Interestingly, the post has actually also an argument for this:

> Experience has shown that, even now, there will still be people explaining in patronizing tones why none of this is real and none of it counts. If such people were capable of being impressed by anything that happens in the empirical world, of updating on anything, they would’ve already been impressed and already updated several years ago, long before things had reached the point of an actual Mathocalypse.

> So, they’ll say, maybe the alleged solutions are not solutions at all, but just “AI slop.”

It's on OpenAI and Anthropic to prove that they obtained these results legitimately and credited all researchers who deserve credit. They do not get the benefit of the doubt.

But if you think they got them illegitimately, then how did they get them? And why are mathematicians reacting to this as a sudden explosion of new results that have resisted sustained effort? Where is the sudden productivity rise coming from?

I'd say it comes from the same mathematicians that were strongly encouraged to use the machine to solve their problems for the last 2 years or so.

There's clear benefit in a babelfish that can coordinate disparate efforts, the only problem with the current iteration is giving credit to said efforts.

Google went quite far down the road to hell, but stopped short of taking credit for websites' content since the company understood that poisoning the well only goes so far. At this point, one can safely conclude that _Chat_GPT was an intentional attempt to squeeze out more data once they mined the internet dry.

> But if you think they got them illegitimately, then how did they get them?

Obviously they stole them from the Proof Fairy.

It's grapes so sour they could etch metal.

Have you actually read the article? It's been actually written, among the other things, because the author's wife has been trying to solve one of the problems for her whole life.

> I think the next step is to demand that proofs either be human-scale or they prove that a human-scale proof is impossible and the machine proof is as good as it gets.

> I suspect that's possible without tripping over the halting problem. (But I can't prove it.)

I doubt that it is. For the language of proofs to be powerful enough to be able to express an arbitrary proof it would have be Turing Complete. Proving that a proof is the smallest proof of a given concept (i.e. there is no smaller human understandable proof) would then be proving the minimality of a program in a Turing Complete language.

Surely by the time of the IPO we will know whether the main results are correct, if only because a different AI will have produced a lean proof or found a logical flaw (the second case would be hard to verify but probably not impossible).

Also from what I can tell from the few fields I understand, the proofs aren't that long or complicated they are just terribly written.

Why should that make material difference to the IPO? What is the economic value of those results?

The entire US federal budget for math research is something like $100M annually. And mathematicians in other countries are hardly making bank either. How does one reconcile how the market has historically valued mathematics with the cash-strapped frontier labs ploughing so much money into that enterprise?

The market works in mysterious ways. What companies do for marketing is often irrational, what companies do to attract investors is likewise often irrational, and why investors invest in companies is also often irrational.

Why should that make a material difference to the IPO? Because of the vibes, and investors are indeed all about the vibes.

It works in mysterious ways, but you know exactly it will behave certain way "Because of the vibes, and investors are indeed all about the vibes."?

The first paragraph is describing a general trend over multiple events across multiple agents. Between zero and three of these can be true for any transaction across every transaction.

The second paragraph is specific to OpenAIs behavior.

> what companies do to attract investors is likewise often irrational, and why investors invest in companies is also often irrational.

Note that the cool thing about rationality is that it does not depend on transitivity. If what companies do to attract investors works, then it is in fact rational of them, regardless of the rationally of investors.

They're burying any doubt that the models are capable of superhuman performance on intellectual tasks. Neural nets aren't calculators, and were notably poor at mathematical reasoning tasks for a long time. Now they're not, and the labs are proving that by chewing through what would ordinarily be decades of progress in a month. And the reason to go for math in particular is because there's no wiggle room. You can't just dismiss it as hallucination.

If the models can do this, they're almost certainly good at just about everything, because the reasoning and creativity required to solve these problems will translate. And even if they were only good at this stuff, that's still a tremendously valuable thing, because quantitative reasoning and analysis is the bedrock for many, many industries.

oAI is gunning for the largest IPO in history at this point, and they might actually get there.

> If the models can do this, they're almost certainly good at just about everything, because the reasoning and creativity required to solve these problems will translate.

The "then" in your "if-then" bears a heavy load. Why would society assign so little economic value to pure mathematics if the skills for proving math theorems translate to massive value in "just about everything"? Would you expect top mathematicians to cure cancer if you transplanted them from the math department to a medical research lab?

Do you think mathematicians are not already working on cancer research? There's quite a bit of heavy math in biostatistics, medical imaging, machine learning, etc.

I'd assume that the majority of people who study math take their skills and move onto some related STEM career that isn't pure math. Academia is incredibly small and competitive.

Because research mathematics is a subset of all quantitative work that gets done, but it's by far the most technically difficult subset. If the models can handle research grade math and produce ironclad proofs, they can probably handle the quantitative side of just about any discipline in a trustworthy fashion. Think about how many dinky spreadsheets have gone on to become critical tooling for large organizations. Even if you consider that many disciplines hide technically demanding work behind tooling (e.g. essentially no one is writing a stiffness matrix FE routine by hand), this model would be capable of writing a direct competitor from scratch to produce the same result.

All of STEM relies on mathematical analysis, and new models are now superhuman at that. And yeah, I'd go a step further and say that the reasoning and creativity required to solve cutting edge math problems probably does translate to other tasks like interpretation of the law, or medical diagnosis, or accounting, etc., for the same reasons that I think most top tier mathematicians would excel at those tasks were they so inclined.

That sort of worked for Eric Lander but as he moved higher up in the bureaucracy, he found himself suddenly having to manage people who weren't nerds like him. He was bad at that had to step down.

American mathematician Jim Simons was worth some $31 billion at the time of his death in 2024. The lack of economic value in pure math doesn't mean that applied math is of little value. Physicists and mathematicians with PhDs "sell out" to join Wall Street as quants and make a killing there, Jane Street is full of them.

> If the models can do this, they're almost certainly good

I would argue that "good at math" was a short hand for "good at X" because mathematicians were historically good at engaging with very complex ideas, distilling them and coming up with precise and concise answers they could validate by themselves.

Given that AI solutions are described as "psychedelical" and they rely on the outside source to validate the result, I don't think the same logic could apply to them.

> I think the next step is to demand that proofs either be human-scale or they prove that a human-scale proof is impossible and the machine proof is as good as it gets.

Who do we demand this from? The AI companies? Or the mathematicians who are worried they will have nothing left to do?

From the entity that is producing these proofs, obviously.

As the old saying: great claims require great evidence.

Ask away. They've dropped the mic, as far as they're concerned; they're not going to worry about what you do with it, or if you don't understand it.

That's the best definition of slop I've ever read.

They still have the mic; I've been told there are another two such proof drops coming.

We should consider the possibility that at some abstraction levels, we can safely stop chasing "clarity" or "coherence" which is circularly defined in such a way that it's capped by human processing power.

Developers and people in CS in general seem to have gotten used to the idea that most productive SWEs don't need to exactly know how to produce assembly or trace every branch prediction or even most of the optimization the CPU (or even their compiler) is running. Mathematicians will get there.

CS got that idea from mathematics. Theorems (with the definitions required to state them) are supposed to be self-contained units. Once the general consensus is that a theorem has been proven correct, people can use it without understanding the proof. Of course, people still want to understand how things work, and it often makes sense to understand them a couple of layers below the one you usually work at. But at some point, you should stop distracting yourself with irrelevant details and focus on your actual work.

Thing is that many of the theorems here are not useful work in and of themselves, but were posed as research problems because it wasn't clear how they could be resolved with current techniques, implying that the process of trying to find a proof might result in new techniques. It's those new techniques that are the actual goal, but if they can't be easily extracted because the proof isn't structured to enable this, that's a bit of a headache.

I've very aware that human cognition has limits.

But it doesn't follow that these proofs - or any proofs - are automatically on the far side of that limit.

The human usefulness of a proof depends entirely on its human legibility. Much of the value of proofs is in inventing new techniques and concepts and having new insights into relationships. Occasionally you get some game changing insight into practical physics or engineering. But that's rare.

Without that, proving or disproving a conjecture is an excuse for new and original thinking.

Compilers are not the same problem. The point of code is to produce reliable-ish consequences from various possible inputs. It's not a creative exercise in logical consistency, which is what maths proofs are, ultimately.

> Developers and people in CS in general seem to have gotten used to the idea that most productive SWEs don't need to exactly know how to produce assembly or trace every branch prediction or even most of the optimization the CPU (or even their compiler) is running.

That's because there's a bunch of people who work on that stuff. Just because web developers don't care about it doesn't mean it doesn't exist. Utter magical thinking.

You seem to be confusing your quantifiers a little. (Not all SWEs must understand all CS) does not imply (there can exist parts of CS that no SWE understands).

Reply on news.ycombinator.com