Hacker News Reader

Comment by p-e-w | Hacker News Reader

Now imagine that PhD “impersonator” has, in the past few months, made more demonstrable progress in mathematics than anyone in history.

I think that would change the conclusion of the argument a little.

View on HN

Or maybe the PhD impersonator discovered a soundness bug in a component of Lean and was able to exploit it.

With no humans able to understand the proofs the impersonator has produced, there's no way of knowing.

This is true of literally any proof of sufficient complexity, human-authored or otherwise.

It takes time to convey the core ideas. It takes time for other mathematicians to come up to speed on the new techniques and approaches or the novel combinations of existing ones.

The actual experts in this field have asked for the argument to be explained to them, and are now at the point where they believe this is plausible. Another person in this thread has produced a Lean proof and presumably is not trying to pull a fast one on us by exploiting a bug in the solver.

TL;DR chill bro.

There are many independent implementations of Lean's proof checker:

https://arena.lean-lang.org/

It's highly implausible that the same bug is present in all of them.

Is that true? I'm actually asking because all the ones that I have seen mentioned from the arena were generated with Claude and I just checked a few random ones and they all have commits by Claude.

I don't know how much was created by LLMs but can you still call these independent implementations?

Yes? Very little about Claude is deterministic. If given the same sufficiently complicated problem, but via slightly different input prompts, it can generate entirely different code. It would be shocking if they all had a single shared bug.

I don't think it would be that shocking, if it's a conceptual confusion that's easy to make.

If it's a complicated but narrow problem then regardless of the prompt its possible that Claude will always converge to the same solution type from its training data. So it will generate different version of the same code that have the different implementations of the same procedure that 'works' but is incorrect in some subtle way.

If the AI had found a bug, I expect it using the bug to prove everithing and geting 700 pdf per week https://xkcd.com/704/

More realistically, that impersonator has created lots of output, and the correct ones are selectively publicized (and few particularly interesting bad answers).

Yes from a social proof perspective.. not really from an objective truth seeking perspective, the best liar tell truths 99% of the time.

Do you really believe Open AI made more progress in math than any of the human predecessors? Come on.

Galois had built modern algebra before dying at 20. What agents did so far is flash in a pan.

Wait and see when _they_ are 20 years old!

> Galois had built modern algebra before dying at 20.

No he hadn’t. You are clearly consuming mathematics through a pop culture lens.

He should have written longer letters and duelled less.

The recent progress does not imply that the "impersonator" has a deep understanding of mathematics. By formalizing a problem in Lean, constructing the proof is essentially a complex search. Because Lean is the arbitrator of correctness, the "impersonator" can make as many mistakes as they want until they find a solution that passes the checker. That is very different from checking a paper for correctness.

Good luck writing a Lean proof of a nontrivial theorem by giving a keyboard to a thousand coke-fueled monkeys. If only it was that easy.

Strange to be against this when it works so well in other industries.

1. Well, mathematics isn't other industries

2. It really doesn't work well in other industries either.

My point is that the AI agents are not trying things at random.

To an extent, that is what automated theorem provers (e.g., SAT/SMT solvers) do quite successfully. The monkeys have very good heuristics and avoid going down unnecessary paths, but they are still monkeys. Similarly, AI might be very good at recognizing patterns (which is very useful!), but doesn't necessarily demonstrate any kind of real understanding.

> doesn't necessarily demonstrate any kind of real understanding

That is an unfalsifiable non-argument, a thought-terminating cliché.

Not at all. It's an open question and it's also probably semantically ambiguous. It's cliche to the extent that recently it comes up repeatedly. Regardless of all that it's nonetheless a valid question.

Please go ahead and provide a working definition of what "understanding" means, in a way that an information processing system can be objectively classified as "understanding" or "non-understanding".

Bonus points if it is able to discriminate between human understanding and nonhuman understanding, without vaguely referring to biology.

Failing that, the question seems to me unfalsifiable as per Popper.

You seem to be agreeing with me. I said it's an open question so expecting me to rigorously answer it in an HN comment is quite absurd, no?

There's nothing unfalsifiable about pointing out that we don't know something.

Closely related, "is this machine conscious" is an important question when it comes to ethics yet runs into the exact same problem. Yet you can hopefully see the issue with blindly deciding in either direction on that one.

It's not just an open question. It's such a fundamentally vague and imprecise concept, that it is not approachable, even in principle. Just like consciousness, as you correctly point out.

We don't have a tool or a ruleset to determine whether something is "conscious" or "has real understanding", as the other user put it. And, thus, the statement "X has real understanding" is unfalsifiable.

It is also a thought-terminating cliche [0], because by opening that can of worms the conversation is automatically derailed, as we just saw exemplified here.

[0] https://en.wikipedia.org/wiki/Thought-terminating_clich%C3%A...

that's a hard cope. You think humans don't make thousands of mistakes to come up with something good?

Of course humans make mistakes, but (outside of Lean at least) they attempt to solve it with experience, understanding, and a certain amount of creativity instead of mashing things together until something works out.

complex searches are quite valuable in mathematics. For example, Maryna Viazovska's fields medal was for finding the right gadget (roughly, a complex search) to prove optimality results in sphere packings.

Right, my comment was not about its usefulness. I was merely pointing out that those results do not necessarily imply any kind of actual understanding.

Reply on news.ycombinator.com