From informal to formal and back

By Patrick Massot – Laboratoire de Mathématiques d'Orsay, Université Paris-Saclay I will first discuss Verbose Lean, a teaching library where students use controlled natural language and custom automation to write proofs in Lean. The goal of this library is not to make it easy to write Lean code, the goal is to make it easy to transfer proving skills from computer to paper. This library shares many goals and solutions with the Rocq Waterproof library. Then I will discuss Informal Lean, a project with Kyle Miller to turn Lean files into interactive web pages in natural language where readers can choose the level of detail.