r/compsci • u/Common-Energy1072 • 1d ago

3SUM in O(n^1.962)

Deterministic 3SUM in O(n^1.962) for polynomially bounded integers, with correctness and word-RAM running time verified in Lean

X thread

Lean verification and proof

1 Upvotes

52% Upvoted

9 comments sorted by

7

u/jeffgerickson 1d ago

Oh, ffs. Where is the damn paper?

2

u/currentscurrents 8h ago

There probably isn't going to be one, just the lean proof and AI writeup.

By the time an actual human understands the proof and writes a paper about it, someone else will have used the AI to get n1.952 or something, and they'll have to start all over again. The speed and quantity is too much to keep up with.

AI math is probably going to end up being a big repository of Lean proofs, most of which never get individual papers.

3

u/randomsubaccount 15h ago

Lol a week or so late

3

u/currentscurrents 8h ago

No, this is based on last week's result. It improves the bound from n1.9992 to n1.962.

2

u/randomsubaccount 3h ago

Wow, I missed a 9. I played around with prompting using my personal context and got down to 1.9962 the day of the release but I thought it was too incremental to post fully. 3% lower is a much bigger improvement

1

u/currentscurrents 2h ago

I'm really curious now what the true best possible complexity is. And whether it's a neat meaningful number, or an arbitrary constant that's just a best-fit from an optimization process.

1

u/randomsubaccount 2h ago

I agree, I'm keen on pursuing it further as a hobby, it would be so elegant if it turned out to be a very nice rational fraction, that would be very satisfying, but would need a fairly large inductive or representational leap

-2

u/AbnormalConflict 1d ago

eal flex here