lobsters score: 2 · tags: ai, math
Note that they do not yet claim to have finished Lean proofs for many of the write-ups.
score 1 · canonical
Update: some of the claims have been retracted.
Note that some of the claims already had Lean certificates from the beginning. I expect that the majority of Lean proofs are correct. I would not exclude a new Lean bug accidentally found and exploited in a single proof, the model(s) used comes from a family better trained to exploit bugs than to exercise good judgement!
Whether any of the Lean proofs will be retracted (or be widely considered obviously worth retracting) as a mismatch for the problem claimed to be studied is anyone’s guess.
score 1 · canonical
There was a melancholy comment about this on Hacker News that I appreciated:
I spent thousands of hours on that problem. I really enjoyed it. Hearing that it is solved somehow makes me sad in a far-off way, like hearing an ex-girlfriend died suddenly in a car crash. I don’t know, there’s probably a lot of people feeling odd emotions tonight.
score 1 · canonical
I’ve always felt the joy of mathematics was in the labor, never the outcome. Those 1000 of hours of joy don’t go away just because someone else proved the theorem, just as you don’t lose the time you spent with a girlfriend after the relationship ends.
The beauty of mathematics, on the other hand, lies more in the structure than the struggle. This is likely true of other human endeavors: sculpture, painting, literature. Is David beautiful because Michelangelo labored hard to “remove the superfluous”? Is the copy in the Soumaya museum, somehow less beautiful because it is a copy?
The best of artists hath no thought to show
Which the rough stone in its superfluous shell
Doth not include; to break the marble spell
Is all the hand that serves the brain can do
score 1 · canonical