Recent advancements in AI proof generation has reminded me of my experience that mathematics can be thought of as this giant interconnected codebase. Many elementary theorems can be proven without any deep understanding at all, by simply stitching basic facts (properties, definitions, etc.) together. This is how I got somewhat good at my undergraduate functional analysis class: I just saw the design patterns of its "codebase" in my head.
Show more of this post
So what I am getting at here is that we should really stop pretending as if people can predict breakthroughs or estimate the importance/difficulty of problems. The project has been going on for some time, it has plenty of legacy code (not going to disclose what this corresponds to, I don't want to upset some folks) as well as some pretty elegant abstractions and templates (category theory, anyone?). Plenty of maintainers died along the way and their areas have fallen into obscurity. The whole thing is a mess! There was certainly some low-hanging fruit out there, we just didn't have the right tools to examine our codebase and see them. Well, until recently. Similarly to software engineers - mathematicians should evaluate each other based on the overall contribution, and not just per "ticket" (e.g. theorem). Refactoring math, as in simplifying things and making them more readable, is as important if not more important now than ever. This post will be updated, just wanted to share the rough concept first.
