Proofs are written to persuade skeptics—once only human readers, and now also machines. But humans and machines have different needs. What if we want to satisfy both? In this talk, I’ll present two directions for bridging this gap. LeanInformal automatically translates Lean proofs into interactive documents with readable English using classical NLP techniques. Verbose Lean, developed by Patrick Massot for use in education, is a library for writing Lean proofs in a controlled natural language. I’ll situate these tools in the broader landscape of using natural language as an interface to mathematics and explore how they might help humans and machines build theory together. This is joint work with Patrick Massot.