A proof of a statement convinces the person/entity addressed that the statement is true. Intuitively, a good proof is short, and easy to verify. A formal proof must convince an automated checking program (that may have limited resources). This talk discusses why we care about formal proofs, how we can design good formal proofs, and situations where we hit a wall. Bio: Meena Mahajan (BTech and MTech, IIT Bombay; PhD, IIT Madras) s a professor in the theoretical computer science group at The Institute of Mathematical Sciences, HBNI, Chennai. Her research interests encompass many aspects of computational complexity theory, including Boolean function complexity, algebraic circuits, proof complexity, and space-bounded computation. She is a fellow of the Indian Academy of Sciences.