| ▲ | rurban 20 hours ago |
| Lean is doing logical AI, the classical AI part. Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic. Both are AI. |
|
| ▲ | teiferer 20 hours ago | parent [-] |
| 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 19 hours ago | parent [-] | | Finding a path in a maze was AI once. | | |
| ▲ | chpatrick 13 hours ago | parent [-] | | I 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 9 hours ago | parent [-] | | So 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. |
|
|
|
