 As Brouwer later put it, “Formal language accompanies mathematics as a score accompanies a symphony by Bach or an oratorio by Handel”. (Brouwer et al. 1937: 262; translation  mine).[5]  Correspondingly, establishing properties of formal systems may have many uses, but ultimately has no foundational significance for mathematics. In a lecture from 1923, Brouwer expresses optimism about Hilbert’s proof theory, but denies that it would have significance for mathematics: