>>12401780i learned an itp for my bsc thesis. learning the basics and knowing enough to write basic logic and number theory proofs took maybe a weekend, so you can really just try a bunch of things and see what you like best.
in terms of atp, you might perhaps wanna avoid stuff like metamath (very little automation) or agda (little automation, except for proof by reflection).
the best i can recommend is use itps a bunch, identify things that seem like annoying busy work and implement automation to get rid of that specific busy work.
program verification may not be the best for novel automation, given that people have already put lots of time into making that less cumbersome.
if i wanted to come up with something new, i'd probably pick some subarea of cs or maths, try to formalize key results of the field and build automation along the way to make common types of informal arguments less cumbersome to formalize.
e.g., afaik nobody has figured out how to formalize computational complexity theory yet without wanting to shoot yourself while implementing and proving the correctness of typical constructions in the field.
