4 ms·
Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
by teiferer 9mo ago
Calling Lean "AI" is quite a stretch. Though I'm also in the camp that dislikes the inflationary use of "AI" for LLMs, so I have sympathies for your viewpoint.
- baq 9mo agoFinding a path in a maze was AI once.
- chpatrick 9mo agoI think that definition is pretty obsolete for the last 20 years. To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.
- baq 9mo agoSo basically anything we don’t know how to write an algorithm for? I see where you’re coming from - but at the same time it’s actually an AI meme and smells of permanently moving goalposts.