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.
Finding a path in a maze was AI once.