Comment by jdb1729
1 day ago
> It would be good to have a formalised proof of the o(n log n) result, for example in Lean. As far as I can tell, one does not yet exist.
The result is fully formalized in Lean by @platypii and myself (on Mathlib's TM2 machine), with ongoing improvements to the exponent (currently at 1-2^-14.38): https://github.com/platypii/integer-mult-bounds-lean
Contributions are welcome!
[dead]
why does the website force people to log in to see the proofs? also, why does it not have something like a "export all lean" button to download all of the lean code that proves a theorem (dependencies included) so it can be easily checked offline? finally, the campaign you gave has a mission "Integer Multiplication in O(n (log n)^(1-κ)) Time" and it's listed as completed, but i checked the graph and it directly depends on something that's listed as "Open" ("Full multiplication bound at κ = 0.000051016920170078"). is it fair to call it completed then?
It's missing a privacy policy, so not sure why you require login for users
[flagged]
> Why would someone contribute to an AI project without getting paid?
Because there exist people who are in deep love with mathematics, but weren't able to get a research position (or cannot afford to take a temporary position at some university for which they would even have to relocate).
So, your question is more like: why would someone play a video game without getting paid?
Those people generally care about learning, IME. "Why would someone play a video game without getting paid?", more like "Why would someone pay money to have a bot play a videogame without getting paid?". People IRL do, of course; they tend to be antisocial and make the game worse for everyone else.
Notoriety also has value, not that that is OPs motivation, but worth noting
I wouldn't know, I get weekly drops.
For now, there's plenty of mathematics that hasn't been enshittified by AI bros.
For this work, you're either inserting coins into Codex, effectively donating money, or you're shoveling your way through the slop that the purchasers of that repo couldn't be bothered to clean up themselves.
5 replies →
It is just going to help the capitalist of the world. Last time I checked many people are having $0 in their bank balance. Contributing is officially a scam for humanity.
4 replies →
They're all equally contributing to mathematics?
True, but something is qualitatively different. Similar to open-source software projects, where people used to participate for the love of the game. Now that machines are doing the work, there is less human connection and feeling of community.
Why bother contributing when there's no one on the other side. There's value being produced, but the beneficiary is mainly the corporations who run the models. Even if the result eventually benefits society in general, the credit goes to them. Not that "credit" or "clout" means much practically, but there used to be emotional and social value for the people involved.
19 replies →
This is why mathematics are having serious discussions about math without mathematics, right?
The people using AI should be paid well enough that they can justify selling out their peers.
6 replies →
What does AI have to do with it?
Why are you here engaging with humans, if you could ask AI to explain?
Why would someone contribute to open source without getting paid?
Mostly because it's been a social project where humans collaborate with each other. As AI usage expands, though, I increasingly don't expect to be contributing without getting paid.
2 replies →
Why would someone help solve cancer if AI worked on it?
This isn't solving cancer. The payoff is, supposedly, the understanding that the purchasers of that repo didn't care enough to bother with.
Also, I fucking hope society values cancer research enough to pay the researchers. If we don't, maybe we deserve what we prioritize.
Well lets give these models a grand challenge then.
I conjecture the true growth rate is O(n(log(n))^(1-f(n))) where f(n) is a slowly increasing function of n.
So larger the integers, more efficient the multiplication gets.
AIs of the world, make this your target, and have centuries worth of fun!!
You forgot to specify that f(n) approaches 1 so that is an easy challenge
yes f(n) tending to 1 as n tends to infinity is the worthy goal. how slowly it gets there would determine whether the growth is effectively O(n) or something slightly larger but that refinement can come later.