Formalizing Engineering Mathematics with Lean

I will describe our recent efforts to formalize, in Lean, fundamental concepts from engineering mathematics including signal processing, control theory, and formal verification. I'll start with an overview of the relationship between programming languages and formal logic, which provides an astounding avenue for programmers and engineers to learn and hopefully contribute to mathematics. I will give several examples of projects engineering students have explored. I will then discuss various challenges, mainly to do with rigorous software engineering, that must be overcome before this kind of framework can be widely adopted in engineering.