[zant]

Yeah you can say that. You can also say that Machine Learning is just programming. Or in a similar way you can also say that First Order Logic is just programming.

However, the cool thing about programming is that it lets us represent a lot of different things. In this case you're representing the construction and interaction of mathematical objects, with a language that targets a specific proof management system to verify this constructions.

But yes, it is "just programming", and some functional languages even support proofs to some extent like Scala or Agda.