Yes! There are several different languages and systems used for coding proofs. Coq [1] is probably the most well known. But, as you alluded to, it is not convenient (or easy) to code all proofs in such a style.
I recall it was accessible if you had programmed in an ML, start here: https://softwarefoundations.cis.upenn.edu/