6 ms·

Thanks for the reply! I'll read that presentation when I get back. First impression: the author needs to learn about luminance as it applies to readability!

by jfarmer 15y ago

Thanks for the reply! I'll read that presentation when I get back. First impression: the author needs to learn about luminance as it applies to readability! Blue text on black background == headache. When you say "do a better job" what do you mean? I'd love to see papers about it. And yes, in that chapter you learn the field axioms and it's fairly straightforward for a computer to verify the statement given you present it to the computer in the correct way. That's my point, and I think Dan's point, too. Mathematicians don't do math that way. Like I said: "If you see that and think "That's easy enough to express in a way a computer understands, and there are proof verification systems" you're missing the point." As for http://adam.chlipala.net/cpdt/html/LogicProg.html http://adam.chlipala.net/cpdt/html/LogicProg.html, it looks relatively foreign to me. I'm going to read through it and figure it out, but would it helpful for a first-year college student who went from AP Calculus the previous year to Spivak's Calculus the next to be spending their time on logic programming? They've probably never even heard the word "lemma."++ It assumes you're at least a little proficient with the language of mathematics. Pointing to things like Coq as a solution is like telling an average computer user, "Why use Dropbox when you can just use rsync and some shell scripts?" It might be the basis for something better designed, but it's only part of a larger, hitherto undiscovered, solution. ++: I'm describing my experience. Spivak was the first time I was introduced to the proof-as-exercise paradigm that's the cornerstone of every higher-math textbook.

ezyang 15y ago
Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using something like an interactive theorem prover. It makes a bit of the formalism quite clearer.) There has been some push, especially in Europe, for using these programs to prove other mathematics; it is certainly possible, although few would say it is pleasant or resembles how ordinary mathematicians work. But I think that, for specific areas of mathematics, these tools are useful today. Especially when trying to teach students how to think formally; you'll find that formal corresponds closely to how the computer thinks about things (and the whole problem is that mathematicians are not very formal at all.) CPDT is not a good first text; Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ does better for people with less math experience.

by jfarmer 15y ago

ezyang 15y ago

Proof assistants have close ties to logic and type theory, so it's not much surprise that they're quite good for doing this small, subarea of mathematics. (Indeed, I think in the not too distant future we will be teaching logic using something like an interactive theorem prover. It makes a bit of the formalism quite clearer.) There has been some push, especially in Europe, for using these programs to prove other mathematics; it is certainly possible, although few would say it is pleasant or resembles how ordinary mathematicians work. But I think that, for specific areas of mathematics, these tools are useful today. Especially when trying to teach students how to think formally; you'll find that formal corresponds closely to how the computer thinks about things (and the whole problem is that mathematicians are not very formal at all.) CPDT is not a good first text; Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ does better for people with less math experience.