A Formalization of the Laplace Transform and Its Inversion in Lean 4

Abstract

We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through real-variable integration and the Dirichlet integral. As an application, we formalize the Laplace-domain solution of the harmonic oscillator and identify its transform with that of $\sin(\omega t)$. We also discuss the principal analytic and formalization challenges encountered in the development.