K. Buzzard's Mathematical Programming Language
Kevin Buzzard of Imperial College has started a new project of digitizing mathematical proofs. See his site.
It’s more than just digitizing, it’s an auto-checker. Gave a few talks about it too, see here for one video