@johncarlosbaez@mathstodon.xyz @dougmerritt@mathstodon.xyz @MartinEscardo@mathstodon.xyz @andrejbauer@mathstodon.xyz @pigworker@types.pl On the more optimistic side:
there is a lot of structure to mathematics, which is currently not very well leveraged, i.e. Universal Algebra and its many generalizations. But people are working on that (myself included).regardless of what some say, there is a lot of 'computational mathematics', which is currently not well supported by any system, and essentially eschewed by Lean+Mathlib. That requires thinking differently. Again, people are working on that.in fact, there is quite a bit more to math in general -- see the Tetrapod approach for one.
To me, what's really missing are experts in designing UX having a solid look at mechanized mathematics tools. For that to bear fruit, experts in requirements analysis need to better understand the full "mathematics workflow" -- where proof is just one small aspect. It might indeed be the most time-consuming part, but it is not necessarily where the most value lies. [See LaTeX as an example of a strong value proposition that has completely changed the practice of mathematics, but in a surreptitious way, as it is essentially invisible wrt "mathematical thought". Its effect is no less important.]
