Mathematicians aren’t interested in computer proof systems because they aren’t (yet) useful in practice. Proof system people don’t care about “real” math because… it’s too hard? (h/t @JohnDCook for OP)
-
-
Show this thread
-
Resonates with
@michael_nielsen &@andy_matuschak’s point that “tools for thinking” have to be driven by the needs of expert professional users, not someone’s appealing theory of education or cognition or philosophy of math or somethingShow this thread -
(I should say that computer proof systems are occasionally useful for computer system verification. It’s “real math” that they aren’t (yet) useable for.)
Show this thread
End of conversation
New conversation -
-
-
Do you think that there is actual dogmatic belief in the idea that it should be possible to turn mathematical proofs into logical ones? If so, I would be curious to see why.
-
Widely held in the philosophy of mathematics. Seems to be informally believed by many/most mathematicians? I don’t know.
- 4 more replies
New conversation -
-
-
I mean, the exact blog that you link to explains that they have just spend the last year formalizing a large chunk of the undergrad math curriculum, which to me seems to pretty conclusively prove that the mathematical proofs can indeed be turned into logical ones.
-
That’s why I kept inserting “yet.” I am enthusiastic about this project and would like to see it progress more rapidly!
End of conversation
New conversation -
-
-
"Coq is French! Schemes are French too! It’s a match made in heaven!"
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.