[mitchellpkt]

You might enjoy learning Lean, which is a functional programming language specifically for theorem proving. You can tackle interesting types of questions, and it is actively used in mathematics research.

Here's a neat walkthrough from Terence Tao, which might give you a sense of whether it's something that piques your interest: https://terrytao.wordpress.com/2023/12/05/a-slightly-longer-...