4 ms·
> It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed progra
by ogogmad 5y ago
> It looks probable that in the future, the standard way to do mathematics will be by programming it in a proof development system, aka dependently typed programming language.
This is a controversial opinion, and not all mathematicians are enthusiastic about it, whether rightly or wrongly. Michael Harris, for instance, is a major sceptic and opponent.
It is still a very interesting idea. And it has had some notable successes already.
- Ericson2314 5y agoIt's a controversial but good opinion. Mathlib marches on and gets better and better.
- sva_ 5y agoI 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.