161–163 of 163 posts
Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?
The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.
That sounds like PR nonsense to me. These companies have had teams of mathematicians for at least 1.5 years looking to make headlines, and they didn't bother trying all 10 millennium problems? Yeah right.
People seem to be talking about anything except the actual results with this particular announcement. Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.
Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…