![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslToday I spoke to Michiel van Lambalgen about my thesis ideas (among other things).
I told him that I was interested in human mathematical reasoning, formalizing/normatizing scientific reasoning, etc. He referred me to Alan Bundy and his Mathematical Reasoning Group, which turns out to be a huge hit for me, since I'd never heard of him, and I really identify with his research statement.
These are the ideas I've been having in this direction:
"foundationalism": the approach of formalizing mathematical theorems for the purpose of justifying them as "good mathematics", i.e. following from a good set of axioms.
instrumentalism suggests that mathematical structures may be useful for scientific predictions and, (if they correspond to intuitions) even scientific explanations, even when logically not very elegant, e.g. even if they haven't been proven to follow from a good foundation.
Kerber - The design of mathematical concepts (very interesting paper) exhibits a quote against foundationalism:
Likewise, it seems many proof systems are stuck manipulating just one representation. Minsky (no surprise) argues that mathematics must work with multiple representations (I lost the quote, but it probably came from a Bundy paper).
proof plan / proof sketch / proof idea:
formal proofs seem in general to be too low-level to be understood by the reader. "proof plans" (my source here is Bundy) seem to be a solution to this.
"proof sketch" sounds like a similar idea.
"proof idea" (Kohlenbach), on the other hand seems to be the one or two crucial steps in a proof. It's that little piece of a proof which may or may not work when trying to prove a more general version of the theorem.
Calculemus seems like a good place to find people to work with. Ah, today I found out that Jacob is interested in this stuff (as is Henrik)... if only they had advertised the proof assistants course at our institute... (which is a *Logic* institute afterall!) (damn friction of information)
I told him that I was interested in human mathematical reasoning, formalizing/normatizing scientific reasoning, etc. He referred me to Alan Bundy and his Mathematical Reasoning Group, which turns out to be a huge hit for me, since I'd never heard of him, and I really identify with his research statement.
These are the ideas I've been having in this direction:
"foundationalism": the approach of formalizing mathematical theorems for the purpose of justifying them as "good mathematics", i.e. following from a good set of axioms.
instrumentalism suggests that mathematical structures may be useful for scientific predictions and, (if they correspond to intuitions) even scientific explanations, even when logically not very elegant, e.g. even if they haven't been proven to follow from a good foundation.
Kerber - The design of mathematical concepts (very interesting paper) exhibits a quote against foundationalism:
[Goldblatt84]:
It would be somewhat misleading to infer that foundational
systems act primarily as a basis out of which mathematics
is actually created. The artificiality of that view is evident
when one reflects that the essential content of mathematics
is already there before the basis is made explicit, and does
not depend on its existence.
Likewise, it seems many proof systems are stuck manipulating just one representation. Minsky (no surprise) argues that mathematics must work with multiple representations (I lost the quote, but it probably came from a Bundy paper).
proof plan / proof sketch / proof idea:
formal proofs seem in general to be too low-level to be understood by the reader. "proof plans" (my source here is Bundy) seem to be a solution to this.
"proof sketch" sounds like a similar idea.
"proof idea" (Kohlenbach), on the other hand seems to be the one or two crucial steps in a proof. It's that little piece of a proof which may or may not work when trying to prove a more general version of the theorem.
Calculemus seems like a good place to find people to work with. Ah, today I found out that Jacob is interested in this stuff (as is Henrik)... if only they had advertised the proof assistants course at our institute... (which is a *Logic* institute afterall!) (damn friction of information)
