[beernet]

On the one-hand side, it's really impressive how LLMs drive mathematics forward, and this pace is only accelerating very quickly.

At the same time, most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter). LLMs do not care about "elegance" the way human beings do, which is a big advantage. LLMs for mathematics is such a great fit on many levels. Can't wait for a significant breakthrough, prove P=NP and all hell breaks loose.

[HawtAds]

> LLMs do not care about "elegance" the way human beings do, which is a big advantage.

It's just a matter of time before you can post train it for elegance too. Mathematical proofs in particular can be formally verified automatically which is a big advantage.

[travisgriggs]

Why is it “just a matter of time”? Why do we assume and say this?

The amount of times humanity has said this and time itself was not enough of an ingredient to achieve some anticipated outcome are legion. But we filter those out and go back to making more predictions based on the current linear derivative we’re observing.

[ainch]

I'm not sure that elegance will be so easy to train for, the same way that writing skill has plateaued (or arguably declined) since earlier models. "Have you solved the problem" is verifiable, but questions of taste are harder to pin down.

[don_esteban]

You can select for 'short proof', or 'elementary proof', or assign the 'cost' of the proof as a some combination of its length, the number and complexity of the new terms it needs to define, and so on.

This might not help you with finding the proof, but once you have a machine that can produce several different proofs, you can select among them and incrementally polish the best one.

I think this is the 'easier' part.

[ainch]

I'm sure you could select for shorter proofs, but then that might be confounding in its own way. I think it's a general problem for LLMs that taste is both subjective and hard to pin down to a single metric. There's a reason mathematicians talk about elegance rather than brevity. Sometimes a long geometric proof with a simple algebraic alternative is still elegant, or elucidates the problem in a new way.

[don_esteban]

Well, there are not that many proofs from 'The Book'.

We are a bit ahead of time, currently I would settle for 'as easy to understand as possible' proof. Not a long, complicated, inpenetrable, mess, that Lean says is correct, but reading it provides no insight.

[card_zero]

This sounds kind of like unreadable code, though. So it's more than just taste.

[jmalicki]

I've actually been involved in annotation projects doing RLHF to train LLMs to do exactly that. It's not a matter of time, it's already happening - it's just seemingly lower priority than "profitable" projects like post-training LLMs to replace white collar workers.

[tcp_handshaker]

>> post-training LLMs to replace white collar workers.

And I look forward to a single example where this happened....

[pitched]

Before LLMs, empire building was a very large incentive to hire. Teams tended to become larger than they needed to be so the boss feels good about their life choices.

LLMs do not fix this problem, they make it worse. Instead of the team being oversized, they’re now way oversized. It is still in everyone’s best interest to look busy anyways and LLMs do help a lot with that.

[jmalicki]

I'm not saying it happened, I am saying they are working hard towards that goal as a business priority, and spending a lot of money on it.

Software engineers are first, but other fields like finance and radiology have huge targets on them too.

[tcp_handshaker]

No need to downvote. Just provide a counter example...

[don_esteban]

The mathematics is to a great extent about understanding of abstract structures. As humans, we prefer simple structures/proofs (I suspect that is to a great extent because those are easier to understand), and as such find elegance in simplicity.

In fact, the capability of the human brain to understand complex structures and proofs is rather limited.

LLMs (hmm, I would prefer to use 'AI solver', as LLM is nowadays just a part of it) finding a complex proof can mean several things: 1) AI by its nature/construction does not have preference for simple stuff (it 'thinks' differently than human: a human will, in its search for a proof, start by exploring the 'simpler' parts of the proof space, and hence more likely find a 'simple' proof, while a AI might be more target oriented and descend deeply in depth-first-search manner to recursively solve sub-tasks, without much regard about the overall simplicity of the proof). This can be eventually solved, by subsequent 'polishing' passes, similarly as things work in human science.

2) there might simply not exist a simple/elegant proof of a given problem. The world is a complex beast. Its just our brains trying to find simple/elegant meaning/structure, even in places where there is none.

[pdonis]

> most of the proofs I've looked at appear super messy and chaotic to me (while still being correct of course, so it doesn't matter)

How do you know they're correct if they're super messy and chaotic?

[_jayhack_]

formal verifiability e.g. vi Lean

[AlexErrant]

Even Lean has bugs.

> AI "Proves" Collatz Conjecture with Lean 4 Bug

https://news.ycombinator.com/item?id=49101465

[drdrey]

of course it does, but it's still the best thing we have

[KPGv2]

I've driven back roads in Ireland. Super messy and chaotic. I was still able to use a map to get to my destination.

[scarmig]

The beernet conjecture: all conjectures have both messy, ugly proofs, as well as a elegant clean proof lurking behind the scenes.

[don_esteban]

Eh, some conjectures have counterexamples.

This one might be one of those. ;-)

[js8]

I agree, counterexample to P!=NP would be great. I tried but it's a mess.

[layer8]

I’m pretty sure “counterexample” is the wrong word here.

[Good4boothee]

Isn't it a bit Catch 22 anyway? If someone finds a algorithm to reduce some NP task X to class P, then that just means X wasn't a true NP task and P!=NP is still undecided?

[layer8]

If it’s an NP-complete [0] problem like SAT, as many NP problems are, then we are done, because all NP problems can be reduced to it (in polynomial time).

[0] https://en.wikipedia.org/wiki/P_versus_NP_problem#NP-complet...

[Tyr42]

You can prove something is in NP by providing a (polynomial) reduction from a known NP hard task, and vice versa. All the known NP problems (Knapsack, SAT, etc) are mutually reducable in this way, so solving one lets you solve the others. So if X was shown to be NP, then given a polynomial time solution to X, you can stack the polynomial time reduction from X to SAT to solve SAT in polynomial time too.

[SetTheorist]

AIUI if you have an (polynomial-time) algorithm to reduce some NP-complete task to P then you have indeed shown that P=NP.

[subsistence234]

NP doesn't mean "we don't know a polynomial time algorithm for it", it means "a proposed answer can be verified as correct in polynomial time"

[js8]

Why? A counterexample to P!=NP would be a polynomial algorithm for SAT. If it exists, it might be a constructible object.

[layer8]

That’s not a counterexample to P != NP, it’s a proof that P = NP. You can’t prove that two sets are the same by counterexample. What you could do is disprove P = NP by counterexample, by showing that some problem is in NP but not in P.

At best, a polynomial algorithm for SAT would be a counterexample to the claim that no NP-complete problem is in P.

[js8]

Sorry, it seems like nitpicking to me. You haven't shown my usage of the word counterexample is wrong, at all.

I think a proven counterexample to Q is always a proof of not Q.

> You can’t prove that two sets are the same by counterexample.

You can in this case.

> What you could do is disprove P = NP by counterexample, by showing that some problem is in NP but not in P.

You could argue that counterexample is defined in one direction only, by convention, as to which hypothesis is more believed. In that case, my usage would be more valid, because the general consensus is P!=NP.

You could also argue that a counterexample should be some finite, constructible object. But that's actually also in favor of my usage - a difficult class is an infinite set, while an algorithm has a finite description.

Also note that AI can still find the counterexample (the actual algorithm), without proving it is a counterexample. Again, my usage of the word counterexample favors that definition of what counterexample is.

But honestly I think it would be more productive to spend this effort on thinking about actual counterexample to P!=NP.

[kmeisthax]

Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN

[empath75]

That very much does not describe what happened. Someone found the bug and used it to disprove the Collatz conjecture as a demonstration of the bug. Nobody ever claimed it as an LLM proof.

[dcsommer]

Sure they care about elegance, or at least brevity. Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems. It doesn't mean they are perfect at it though.

[windexh8er]

"They" don't "care" about anything. It is a stateless computational run across thousands of semiconductors. There is no objective this software has other than the computational function completing. To care would mean the model would have a level of discernment that goes along with sentience.

[js8]

You are kind of ignoring the Dennett's idea of different stances: https://en.wikipedia.org/wiki/Intentional_stance

You're looking at humans from intentional stance, but at LLMs from design stance, which would be a form of categorical error.

[subsistence234]

The supposed "magicality" of human consciousness is hard to reconcile with evolution -- where on that long path from amoeba to homo sapiens did God (PBUH) implant our connections to the soul realm?

Even evolution-deniers run into difficult-to-justify self-contradictions when trying to explain how the supposed supernatural part of our consciousness is both affecting the natural world and affected by the natural world, but not part of it.

[Someone]

> Minimizing tokens out, or generally "token efficiency," is part of the objective function for these systems.

First time I heard that, and I doubt it. Don’t customers pay for output tokens? If so, why would a company specifically spend time training their LLM to generate fewer?

[yreg]

So they can charge more per token and decrease the pressure on their infra.

[Someone]

Even if you specifically train the model on producing shorter answers, I would think producing good short answers would require more resources just as it does for humans (https://quoteinvestigator.com/2012/04/28/shorter-letter/: “If I Had More Time, I Would Have Written a Shorter Letter”)

If so, charging per output token is the wrong incentive.

[senorrib]

You clearly haven't used Claude to generate code or documentation.

[nelox]

"First rule in government spending: why build one when you can have two at twice the price" - S.R. Hadden

[KPGv2]

Personally, I've found city roads to be more reliable than the private roads where I live.