4 ms·

You can give a try formalizing some basic math with proof assistants. With such an attempt, you will discover that 90% of your time will be spent transforming t

You can give a try formalizing some basic math with proof assistants. With such an attempt, you will discover that 90% of your time will be spent transforming types into other types and working through obvious transformations. And when you are done, the least obvious steps (for your reader) will be hidden in a forest of obvious steps. Suppose that you want to communicate to someone how to get to B from A. You don't tell them "lift your foot in this manner, then lift your other foot in this other manner, go a little left when you see this small obstacle", etc... you assume that they have competence at navigating commonplace obstacles, and give just the directions that they should take at intersections.

valenterry 4y ago
But for math proofs, we shouldn't assume that people have competence of common basic parts. At least not to truly help them gain a good understanding of the constructive proofs. To me, the example is rather to tell them get into the car then press the button and turn the wheel like this and you'll reach your destination. But they won't understand the car and I think they should, because at some point the need to, unless they never dig deeper - but then maybe we don't need to teach those theoretical things from the beginning.
- jhanschoo 4y ago
  > But for math proofs, we shouldn't assume that people have competence of common basic parts. Well, it does depend on the audience you're writing for. So research math doesn't do that, whereas first-year undergrad math makes an effort to. I think it's essential for first-year math programs to have a course where you redevelop basic induction, natural numbers, addition, etc. from first-order logic and rules of inference and ZFC, which I don't think is true everywhere. And there should be an aspect of it that's about converting that formal proof to informal proof given some assumptions about the reader. Beyond this, it starts to get tedious.

valenterry 4y ago

But for math proofs, we shouldn't assume that people have competence of common basic parts. At least not to truly help them gain a good understanding of the constructive proofs. To me, the example is rather to tell them get into the car then press the button and turn the wheel like this and you'll reach your destination. But they won't understand the car and I think they should, because at some point the need to, unless they never dig deeper - but then maybe we don't need to teach those theoretical things from the beginning.

jhanschoo 4y ago
> But for math proofs, we shouldn't assume that people have competence of common basic parts. Well, it does depend on the audience you're writing for. So research math doesn't do that, whereas first-year undergrad math makes an effort to. I think it's essential for first-year math programs to have a course where you redevelop basic induction, natural numbers, addition, etc. from first-order logic and rules of inference and ZFC, which I don't think is true everywhere. And there should be an aspect of it that's about converting that formal proof to informal proof given some assumptions about the reader. Beyond this, it starts to get tedious.