It's odd that functional programming enthusiasts always love to put the mantle of "math" on their favorite functional tidbits, while real mathematicians write imperative, stateful (and often sloppy) Python.
Most of what functional programmers / theorists tend to care about are from sub-fields like logic, abstract algebra and the like.
The "real mathematicians" that you mention are most likely working in other fields like linear algebra, statistics etc. While it is certainly possible that logicians and algebraists work with sloppy python (in as much as they write any code at all), but I don't feel that it had be a great fit.
Here's a paper by the author of this post, formalising a popular Haskell pattern in category theory: https://arxiv.org/abs/2001.07488
EDIT: switched to non-PDF link.