 Although Brouwer developed his mathematics in a precise and fundamental way, formalization in the sense as we know it today was only carried out later by others. Indeed, according to Brouwer’s view that mathematics unfolds itself internally, formalization, although not unacceptable, is unnecessary. Others after him thought otherwise, and the formalization of intuitionistic mathematics and the study of its meta-mathematical properties, in particular of arithmetic and analysis, have attracted many researchers. The formalization of intuitionistic logic on which all formalizations are based has already been treated above. 