Tao has also used "Good Old Fashioned AI" (in the form of Mace4/Prover9) for math research.

https://terrytao.wordpress.com/2025/12/09/the-equational-the...