> I think interactive theorem provers would go a long way towards making children understand symbolic reasoning. I can agree with that, but symbolic reasoning

> I think interactive theorem provers would go a long way towards making children understand symbolic reasoning. I can agree with that, but symbolic reasoning isn't everything. As shown by Gödel, you can't have symbolic system capable of proving every true fact about natural arithmetic without also proving some false "facts" about natural arithmetic. The ultimate game doesn't have rules. On some level, math is just few pieces of meat speculating about abstract notions originating from and tied to their physical experience. Or something like that :)