How useful it is for math student to learn programming to find proofs or counterexamples? I study mathematics and sometimes I have difficulties to find proofs or counterexamples to some problems. Is it useful to learn programming to find counterexamples or proofs? How useful it is for mathematician to learn for example Coq or Lean?
This is pretty much in the realm of opinion, but as a math PhD and a long time CS professor, I'd guess the answer is no. Programming is fun and programming can be useful, but its application to proving theorems in mathematics is very specialized and a bit limited. And it generally doesn't apply to the sorts of things a struggling math student wants to learn.
There are a couple of exceptions in which programming was instrumental in establishing a proof. One is the Four Color Theorem which was originally proved with a computer because of the huge number of different possible planar maps. But mathematicians, like myself, find that proof unsatisfying and would prefer one that was more analytical and which would lead to more insight. But these sorts of cases are very rare.
But, theorem proving, like anything else is a skill best learned through practice. Once you have tried and eventually succeeded at proving some theorems, perhaps after false starts, you will start to gain insight. Every success can lead to the next success. But it is hard work. And the work may not get easier as you go, since you will probably take on harder problems. But practice, practice, practice.
Programming does, however, give you some practice with thinking logically and breaking a hard problem down into smaller, easier, parts. In that sense programming can be a bit helpful. But to learn math, just do math.
On the other hand, there are automated Theorem Provers that can do some interesting things. But their results don't generally lead to the insight into a problem that a mathematician needs and to build one of them requires deep insight to start with.