The development of new and improved proof systems, proof formats andproof search methods is one of the most essential goals of Logic. Butwhat is a proof? What makes a proof better than another? How can aproof be found efficiently? How can a proof be used? Logicians fromdifferent communities usually provide radically different answers tosuch questions. Their principles may be folklore within their owncommunities but are often unknown to outsiders.This book provides a snapshot of the current state of the art in proofsearch and proof production as implemented in contemporary automatedreasoning tools such as SAT-solvers, SMT-solvers, first-order andhigher-order automated theorem provers and proof assistants.Furthermore, various trends in proof theory, such as the calculus ofinductive constructions, deduction modulo, deep inference,foundational proof certificates and cut-elimination, are surveyed;and applications of formal proofs are illustrated in the areas ofcryptography, verification and mathematical proof mining.Experts in these topics were invited to present tutorials about proofsduring the Vienna Summer of Logic and the chapters in this bookreflect their tutorials. Therefore, each chapter is intended to beaccessible not only to experts but also to novice researchersfrom all fields of Logic.