[gaogao]

> I wonder if we'll ever use AI to write code in dependently typed languages

Yeah, I write code in Lean with AI pretty frequently lately