El artículo «Teaching mathematics with Lean: Interactive theorem provers in the classroom», publicado en la última edición de las Notices of the American Mathematical Society, explora el potencial de Lean —un asistente de demostración interactivo— como recurso didáctico en el aula de matemáticas.