Comment by gewetensleegte
3 hours ago
> 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?