A conventional symbolic proof seems at first sight to have quite a different character from the ‘hands-on’ virtual-reality sort of proof. But we see now that they are related in the way that computations are to physical experiments. Any physical experiment can be regarded as a computation, and any computation is a physical experiment. In both sorts of proof, physical entities (whether in virtual reality or not) are manipulated according to rules. In both cases the physical entities represent the abstract entities of interest. And in both cases the reliability of the proof depends on the truth
...more
