I have been wondering why programming is so much more accessible than mathematics to many, considering programming is in some way also a kind of mathematics.
I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it.
So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.
I think some of it may have to do with the fact that in programming, one can get immediate and non-judgmental feedback about the correctness of ones solution. In mathematics, it's usually a lot more difficult to verify a solution if you don't already know the answer, so you're dependent on people for it.
So perhaps, interactive theorem provers may make mathematics a lot more accessible. But I hope the art of doing it with pen and paper doesn't get lost on us with it.