|
|
|
|
|
by znfi
3089 days ago
|
|
Not really a mathematician, so take this with a grain of salt. I would guess there are probably several different reasons for "looking down" on proof assistants. On the one hand we have something like the 4-colour theorem where there is some kind of "proof", which is very large and incomprehensible. This is probably unsatisfactory to many because one is not really interested in just knowing that something is true, but ideally one also want an understanding of "why" something is true. This is, to various degrees, achived in more standard proofs. Another reason for disliking proof assistants is probably that they simply are very cumbersome to use and not very much can be proven with them so far. I would guess that even if you could get someone to admitt that the idea is cool and could be very useful, it's just not practical and for most people in mathematics it's just a distraction from what they are trying to work on at the moment. Compare with trying to convince someone that a flying car is really cool, yeah, sure, it probably would be, but so far it's basically sci-fi. If you want to work on building this, great, but most commuters will probably "look down" on your idea if you start bugging them about it. |
|