&gt; I think interactive theorem provers would go a long way towards making children understand symbolic reasoning.<p>I can agree with that, but symbolic reasoning isn&#x27;t everything. As shown by Gödel, you can&#x27;t have symbolic system capable of proving every true fact about natural arithmetic without also proving some false &quot;facts&quot; about natural arithmetic.<p>The ultimate game doesn&#x27;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 :)