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 corre

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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...