Harvey calls the claimed o(n log n) integer multiplication bound from an AI math dump plausible but unchecked
- David Harvey of UNSW Sydney says the o(n log n) integer multiplication claim from a recent math dump by a major AI company is plausible, though he has not checked most of the details.
- The claimed bound is O(n(log n)^(1-ε)) with ε set to 2^-182 in the first writeup, which Harvey argues is an exponentially larger gain than any earlier improvement over O(n log n).
- The result builds directly on the 2021 algorithm by Harvey and Joris van der Hoeven, and a Hacker News commenter reports it has been fully formalized in Lean with the exponent improved further.
- Harvey says he used Claude Fable 5.1 for discussions that helped him understand the new algorithms, while typesetting and proofreading were also AI-assisted.
Hacker News 의견들
Note the title says O(n log n), but the real claim is o(n log n), which is a strict subset. We already had O(n log n) via FFT.
For those of us not in the field, O means grows no faster than some constant times n log n, while little o means grows strictly slower than every constant times n log n. That's the whole difference.
I really like the writing in this one. The part about colleagues calling the company nefarious, then saying who got there first doesn't matter, is pretty honest.
That 'I do not blame the Company' line reads a bit too neat to me. Noble framing from someone whose field is being reshaped by that same company.
I haven't read the paper either. I asked Fable to explain TC26a and it says the argument is correct. Still feels odd to trust the explainer over the proof.
Why not use the tools if they can explain it? A human still has to check it, and Lean proofs are the only thing that really settles this.
A convincing impersonator of a math PhD tells you nothing about validity, so 'I understood it' carries no weight by itself.
Someone already formalized this in Lean on Mathlib's TM2 machine, and the exponent is now down to 1-2^-14.38, so the check is getting done.