A Theorem is like the specifications for a machine. A Proof is like the design. One may buy a machine off the shelf and use it (use a theorem without knowing its proof). Or one may be interested in constructing it by oneself by following the design (check the proof). Or for that matter, one may wish to construct ones' own design which confirms to the given specification (find ones' own proof).

While following the design, one must allow for the possibility that all parts as specified may not be available and then these parts would themselves have to be obtained by one of the above three methods. Thus a considerable amount of ingenuity and labour is likely to be demanded for this process; more so if the machine is complex and made of many parts. Thus there is not as much difference between the latter two methods of obtaining a machine (checking/finding a proof) as may appear at first glance.

Another problem that is likely to crop up is that the design can never be ``complete'' in all aspects. This because many parts would not be given in terms of sub-designs but only as specifications. Indeed for any complex machine it would be impossible to give the sub-design of each component, since this would require the sub-sub-design of a sun-component (or tool) and so on. A certain similarity of the toolkit and inventory of the designing and assembling workshop; and a certain amount of skill in designing on the part of the assemblers must be assumed.

The only way that the robust-ness of a design (correctness of a proof) can be verified is if a number of (100%!) indigenous assemblies are performed by various people. Unfortunately, in these days of liberalisation the old notion of import substitution has given way to elimination (indeed active discouragement via TRIPS) of duplicate efforts!

The above analogy breaks down in one obvious way. We have not said how one is to ``convince'' oneself that the machine that one has built indeed confirms to the specifications--except through use. Else there should be some (metamathematical) proof that constructions as performed do lead to the required result.

One situation where this analogy does have some value is in understanding why one group of mechanics (physicists) is unable to convey their designs to another (mathematicians); moreover, the complaint is of bad design from one end and bad tools from the other! In case two groups of mechanics have developed their own tool boxes and parts inventories, they would be loathe to re-construct (right from scratch) the entire such infrastructure of the other team even if they find that there are certain good features of some complex machines of the other side that this side would like to have. The synchronisation of the two infrastructures is likely to be a long drawn out (and perhaps never ending) affair.



Kapil Hari Paranjape