I said 30 years, because that's for how long I am a participant in the field. I have a PhD in ITP, and yes, I am pretty confident that automation is a big part

I said 30 years, because that's for how long I am a participant in the field. I have a PhD in ITP, and yes, I am pretty confident that automation is a big part of ITP now. Maybe not so much if you are into constructive type theory, that field is always a little bit hesitant to use the full power of anything. The only one lying here is you. To yourself. By the way, AI can come up with conjectures just fine. I might not be interested in most of them, but then again, I am not interested in most conjectures humans come up with.