358 karma · joined July 10, 2025
This is not true in many jurisdictions.
"Chess players who don't use engines will be left behind", they say. I can't emphasize enough how much I hate it when I hear/read shit like that because I'm pretty sure, in fact, that what will happen is the exact opposite.
People who rely on engines are the ones who will be left behind. They'll forget how to think, how to move the pieces, how to solve a simple straightforward mate in 3, how to tell victory from stalemate... they'll forget how to fucking LEARN. I think that's the part that makes me the saddest. What a beautiful thing it is just to play chess.
If you think Deep Blue can do better than you, why would you just let it? Why wouldn't you aim to be better, to learn how to be or do something that a chess computer would never do?
Occasionally, inspecting that proof term is useful to see what happened in a proof.
Then again, I also like dependent types.
The blog article author is saying that Lean is like a younger child (that needs more intermediate steps explained), stores proofs more inefficiently (taking more memory) and that its computer proof language is harder to read for humans. Additionally there is a technical point about dependent types, which are the principle around which the computer proof language is organized (the same way a programming language might be organized around object-orientism).
But I am not sure you can compartmentalize the specific skill we can out-source to AI. I would not agree with "you don't need to be able to think in your head."
It's on like place 10 out of 180, which makes it one of the least corrupt places.
It also has some surprisingly non-boomer departments, like the Sovereign Tech Fund. Either way you need to celebrate police doing good things and immoral actors being exposed, it can only have good outcomes.
Perhaps it deters them, or deters the next generation of such hackers. Or at least it makes their life less enjoyable, which is fair since they were only able to afford their travels due to their illicitly acquired wealth.
The same thing is true with computers. Imagine all the nice things we could have if we didn't have to worry about people abusing the systems we build.
Makes you wonder if the investigators discovered this independently, or decided to maybe ask the hackers already involved in defending against them for help...
Or more poetically, "if my grandmother had wheels she would have been a bike[1]" is a folk wisdom precisely because it makes so much sense.
This is not to defend the study, because asking AI has a lower barrier to entry.