Comment by hardbass
6 hours ago
Anyone can solve any problem they want and release it. Nobody is defending multibillion companies, they are pointing out hypocrisy when the same would be celebrated of it was some academic mathematician who also used ai released a solution vs open ai or any other entity doing so.
> Anyone can solve any problem they want
I'm pretty sure the multi billion dollar company has been throwing some of those multi billions at it
> and release it
"it" being a Lean proof that shows they could, technically, get a real mathematician to write down a real Math proof that could actually get published and be useful, right?
"it" being, a bunch of busy work for real mathematicians without the actual pay-off of discovery?
Nobody is forcing anyone to look at anything. Most human math papers don't even have a formal proof and now people are whining when a company goes beyond and releases formal lean proofs.
Do you disagree with the four color theorems proof? Do you know how much compute was used for that?