[wisnesky]

Yes, in the sense that "math is programming paper instead of computers", being better at one translates to being better at the other. This intuition can even be made precise via the "Curry-Howard isomorphism", upon which "proof assistants" such as Coq are built.

[westurner]

Lean mathlib was originally a type checker proof assistant, but now leanprover-community is implementing like all math as proofs in Lean in the mathlib project.

Lean (proof assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)

"Lean mathlib overview": https://leanprover-community.github.io/mathlib-overview.html

"Where to start learning Lean": https://github.com/leanprover-community/mathlib/wiki/Where-t...

leanprover-community/mathlib: https://github.com/leanprover-community/mathlib