 Proof theory, as we described it, deals primarily with formal proofs or derivations. Hilbert aimed, however, as we pointed out in  section 1,  for a more general analysis of ordinary, informal mathematical proofs. For Gentzen in his 1936, “the objects of proof theory shall be the proofs carried out in mathematics proper” (p. 499). The aim of Hilbert and his collaborators was undoubtedly to achieve a deeper mathematical and conceptual understanding, but also to find general methods of proof construction in formal calculi. This is now being pursued in the very active area of using powerful computers for the interactive verification of proofs and programs as well as the fully automated search for proofs of mathematical  theorems.[34]  That can be pursued with a cognitive scientific purpose of modeling mathematical reasoning (see Sieg 2010 and Ganesalingam &amp; Gowers 2017). It is clearly in the spirit of Hilbert who articulated matters in his second Hamburg talk of 1927 as follows: