On: “Math 2.0” will need to value mathematical progress more holistically

[auggierose]

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.

[oliculipolicula → auggierose]

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