Jeremy Avigad's "Mathematical Method and Proof"
Jeremy Avigad's "Mathematical Method and Proof" exposes lots of the ideas that I've been writing about time and time again on this blog, under the tags formal_math and formal_ed (for my education-related formal dreams / practical epistemology).
Here's some ideas we have in common:
* we're interested in the program of creating a theory of mathematical understanding ( here; I've also blogged about a program for understanding scientific understanding)
* "proof ideas" (Kohlenbach) as an application of proof theory (what about formalizing the notion of "proof identity"?)
* if would be good if theorem-provers used cognitive representations more (Kerber)
* to be finished...
here's a thought:
the challenge of doing mathematics is often the challenge of expressive one's intuition... like remembering a word that's at the tip of your tongue.
Here's some ideas we have in common:
* we're interested in the program of creating a theory of mathematical understanding ( here; I've also blogged about a program for understanding scientific understanding)
* "proof ideas" (Kohlenbach) as an application of proof theory (what about formalizing the notion of "proof identity"?)
* if would be good if theorem-provers used cognitive representations more (Kerber)
* to be finished...
here's a thought:
the challenge of doing mathematics is often the challenge of expressive one's intuition... like remembering a word that's at the tip of your tongue.