logoalt Hacker News

auggierose • today at 7:48 AM • 1 reply • view on HN

A correct solution verified in Lean will count in perpetuum. It is fine if you want more, but an achievement is an achievement, even if it is by AI.


Replies

oliculipolicula • today at 10:16 AM

Hmmmm. It feels right that discovery is much more meaningful than achievement. "Bullshit lean proof" or "bullshit achievement" smells like it. "bullshit discovery" smells like a front-handed insult