[zozbot234]

Automated reasoning is usually included in AI (Lean4 has tactics so it qualifies as such) but it's also quite different from the ML stuff that's the more usual kind of AI these days.

[alexvitkov]

Things usually stop being considered as AI when they start working.

[rprenger]

You can have both! LeanDojo: Theorem Proving with Retrieval-Augmented Language Models https://arxiv.org/abs/2306.15626 (shameless plug)