 It is clear to us, and it was clear to Hilbert, that mathematical thinking does not proceed in the strictly regimented ways imposed by an austere formal theory. Though formal rigor is crucial, it is not sufficient to shape proofs intelligibly or to discover them efficiently, even in pure logic. Recalling the principle that mathematics should solve problems “by a minimum of blind calculation and a maximum of guiding thought”, we have to investigate the subtle interaction between understanding and reasoning, i.e., between introducing concepts and proving theorems.