I attended a conference on formalization of mathematics. The challenges to progress appear to include the following
The diversity of topics (both depth and breadth) is huge.
The variable level of formalization (from natural language to Latex to Constrained Natural Languages to Computer Algebra Systems to Proof assistants.
Addressing all the requirements (readability, conciseness, preciseness) is infeasible with current techniques, so selecting any potential solution is suboptimal. Investing resources (time, attention, compute, creativity) in a suboptimal solution is an opportunity cost.
There is more brain power than staffing. Good ideas don't get implemented because hiring software programmers isn't accessible
The staffing that is available is graduate students. These are neither domain experts nor experienced programmers
The degree of automation for projects varies. What is considered hard or scalable depends on who is doing the work.
Design decisions are driven by the specific problems being solved. A "universal" and comprehensive approach incurs inefficiency in any given domain.
The degree of software development best practices varies (linting, continuous integration/continuous deployment, use of version control)
The diversity of implementation choices (Python, Haskell, Coq, C, C++)
Inventing novel domain specific languages is easy for this community, further mudding the options
Standard (basic) math is not exciting to build a product around
Maintenance of software and databases is not exciting research
There are a variety of databases which hold proofs: