EPFL Seeks Postdoc for Formal Verification, Algo Discovery in Numerical Analysis

The Chair of Numerical Modelling and Simulation at the Swiss Federal Institute of Technology in Lausanne (EPFL) has announced a postdoctoral research position dedicated to integrating formal verification and artificial intelligence into numerical analysis. Located in Lausanne, Switzerland, the role invites researchers to pioneer a new scientific trajectory that explores how proof assistants such as Lean and advanced machine learning tools can transform the design, discovery, and validation of numerical algorithms for partial differential equations. Successful candidates will establish and direct an independent research line in close collaboration with faculty members. The position deliberately avoids a fixed project scope, instead emphasizing exploratory experiments to identify concrete applications where formal methods enhance mathematical rigor and where AI accelerates algorithm discovery. Potential research avenues include the formal verification of stability and error estimates for finite element methods, as well as the AI-driven development of novel discretization techniques for challenging mathematical models, followed by rigorous automated validation. The role requires strong expertise in numerical analysis, mathematical proofs, and familiarity with computer-aided theorem proving or machine learning frameworks. The appointee will be responsible for disseminating findings through peer-reviewed publications and international conferences. EPFL offers a flexible start date ranging from immediate deployment to a mutually agreed timeline, with ongoing evaluation of applications until the position is filled. Interested researchers must submit a curriculum vitae, a motivation letter outlining a specific research question bridging numerical analysis with formal verification or algorithm discovery, and contact information for three referees. This initiative reflects a broader shift in computational mathematics toward hybrid methodologies that combine human-driven mathematical insight with automated reasoning and data-driven discovery. By targeting partial differential equations, a foundational area in scientific computing, the position aims to establish reproducible workflows that reduce human error, accelerate method development, and strengthen the theoretical guarantees underlying numerical simulations. Applications remain open until the role is secured.