I work in mathematical logic, axiomatic set theory, and formal mathematics. I have constructed numerous minimal models of set theory for large cardinals and used them in conjunction with forcing techniques to determine the strengths of infinitarry combinatorial principles. In computability theory I have started the field of infinitary calculations with ordinals.My contribution to TRA1 is the project Naproche (Natural Proof Checking) whose aim is to combine formal mathematics with natural language. We have developed a proof assistant Naproche-SAD that accepts nearly natural input texts and checks them using strong automatic theorem proving techniques. We shall formalize comprehensive mathematical theories from undergraduate textbooks. Our techniques can be combined with other systems in formal mathematics and they have didactical applications. We collaborate with computer linguists and also with philosophers of mathematics.