Comment by rurban
2 days 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.
2 days 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.
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.
Finding a path in a maze was AI once.
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.
1 reply →