This is a wonderful series of articles and I find myself nodding along with most of it. However, these lines really made me cringe: A child was sent to me fo

This is a wonderful series of articles and I find myself nodding along with most of it. However, these lines really made me cringe: A child was sent to me for tutoring because of failing a geometry class, and gave this excuse: " I must have been absent on the day when they explained how to prove a theorem." No wonder this child was confused—and seemed both amazed and relieved when I explained that there was no standard way to make proofs—and that “you have to figure it out for yourself”. One could say that this child simply wasn’t told the rules of the game he was asked to play. However, this is a very peculiar case in which the ‘rule’ is that there are no rules! (In fact, automatic theorem-provers do exist, but I would not recommend their use.) I think interactive theorem provers would go a long way towards making children understand symbolic reasoning. The way these programs work is that you have feedback available at every step of a proof. Children can learn basic causal relationships by looking at the world around them. By visualizing the basic relationships between logical formulae you can similarly learn to inuit the effects of reasoning steps. Interactive theorem provers provide the visualization. The game has rules, and you can learn them.