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.
Programming is very useful in the process of conjecturing, and to some extent even in proofs.
Here are some examples from my own research, in theoretical computer science and combinatorics:
An algorithm for maximum coverage (a basic combinatorial optimization problem) employs a non-standard objective function, with finely tuned parameters. These parameters were obtained by solving a linear problem on a computer. The parameters depend on $n$, so I solved the linear programs corresponding to small $n$, and generalized the solution. The solver also found the tight constraints, and this was very instrumental in the proof.
The construction of the Gelfand–Tsetlin basis for the Johnson scheme (equivalently, a canonical eigenvector basis for the Johnson and Kneser graphs) came out of some experimentation in a computer algebra system; I don't know whether you consider this programming.
Several papers in social choice theory aimed at proving phenomena which were first observed experimentally; this required programming in an efficient language.
Optimal gadgets in a paper in circuit complexity were found by exhaustive search using an efficient computer program.
I would say that programming is a useful skill, at least in certain areas of mathematics.
The only thing that programming can do for you is teach you logical thinking, if you have problems there.
The computer won't let you use assumptions or take shortcuts. You have to create a complete, logical sequence of instructions to get from the problem to the solution. And that skill is of course also needed for mathematical proofs.