Yes, people are using the programming language Lean for that, and there are a few less popular alternatives as well.

Fundamentally, there is a one-to-one correspondence between mathematical proofs and programming. Proofs are isomorphic to type checking.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...