QED: a conversation about math and math education

Join MoMath’s 2023-2024 Distinguished Visiting Professor Ingrid Daubechies for an hour of math learning, designed with you in mind.  This month, Ingrid welcomes Colleen Robles, professor of mathematics at Duke University where she led a team of undergraduate students who developed a teaching aid for an introductory linear algebra course.  Using Lean, an open software tool that allows encoding formal proofs in its own functional programming language, the package they put together plays out like a game that allows students to write formal proofs in linear algebra.