![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslJeremy 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.