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