I think the same problems manifest in math, but to a different degree and in a different way. We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.

But I don't think that math education is generally very successful at teaching people math, as described in Lockhart's Lament: https://www.maa.org/sites/default/files/pdf/devlin/Lockharts...

My suspicion is that a big part of the issue is the way math is presented early on is really tedious and boring to a lot of people, in a way that could be addressed by theorem provers. I think something like the Xena Project https://xenaproject.wordpress.com/what-is-the-xena-project/ is potentially an interesting development in that regard (though more for undergraduate math than grade school math).

I also don't think this is anyone's "fault" really. I'm more interested in figuring out what might make things better than assigning blame. Nor do I think I personally can fix it single-handedly with a new programming language. If Yatima can move the ball forward a little bit by eventually contributing to a few people learning and falling in love with programming and math, that's more than enough for me.