Aristotle is doing the matching AI part, the modern LLM approach, previously called fuzzy logic.
Both are AI.
To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.
