this might seem normal but perhaps not in mathematics? There's the story about homotopy type theory that first had to be invented including a supporting program

this might seem normal but perhaps not in mathematics? There's the story about homotopy type theory that first had to be invented including a supporting programming language to formalize and automatically error check proofs, which is still a niche topic in maths (because it seems faster to think barely, I gather. Edit: and because of the problem of bootstrapping such a system and Not Invented Here syndrome).