Postdoc in Formal Verification and Algorithm Discovery for Numerical Analysis, EPFL
Job Description
EPFL’s Chair of Numerical Modelling and Simulation is hiring a postdoc on formal verification and algorithm discovery for numerical analysis, using proof assistants such as Lean and Rocq. The call is open until filled.
At a glance
- Post: Postdoc in Formal Verification and Algorithm Discovery for Numerical Analysis
- Where: Chair of Numerical Modelling and Simulation, EPFL, Lausanne, Switzerland
- Pay: on the EPFL scale for this grade; the advert gives no figure
- Closing date: none given. EPFL reviews applications as they arrive, so the post is open until filled. We re-check these listings about every 30 days
Read the official EPFL advertisement before you apply.
The project
The chair designs and analyses numerical algorithms for partial differential equations, with research oriented towards techniques that integrate numerical simulation with geometric modelling and processing.
This post brings proof assistants into that work. Tools such as Lean let a mathematical argument be checked by machine, line by line. Applying that to numerical analysis is harder than it sounds: the interesting theorems involve real numbers, approximation and error bounds, and formalising them takes both the mathematics and the proof engineering. Algorithm discovery is the other half, where the machine helps find the method as well as check it.
What you need
- A PhD in mathematics, computer science or a closely related field
- Experience with a proof assistant such as Lean or Rocq, or strong numerical analysis and a willingness to learn one
- Read the official advertisement for the full requirements
Pay and conditions
EPFL pays doctoral assistants and postdoctoral researchers on published Swiss federal scales, which are among the higher ones in Europe. This advertisement states no figure, so check the scale for your grade and the cost of living in Lausanne before you decide.
How to apply
Apply through the EPFL careers page for this post. The advertisement gives no closing date. EPFL reviews applications as they come in, so apply early.
Browse more research jobs on ResearchJobs.in, or search our Find a supervisor page.
Hiring institution: École Polytechnique Fédérale de Lausanne (EPFL)
Official advertisement: careers.epfl.ch
How to prepare for this application
- Show a formalisation you have done. Even a small Lean project says more than a description of interest.
- This is an unusual pairing. Numerical analysts who can prove in Lean are rare, which is the opportunity.
- EPFL works in English. Research and teaching at this level run in English, so French is useful but rarely required.
- Doctoral candidates apply twice. A lab offer at EPFL is normally followed by admission to a doctoral programme, so check the programme's own requirements too.
About EPFL
The École Polytechnique Fédérale de Lausanne is one of Switzerland's two federal institutes of technology. It has more than 6,500 staff and over 18,500 people on campus, including more than 14,000 students and 4,000 researchers from over 120 countries, with sites at Lausanne, Neuchâtel, Fribourg, Sion, Geneva and Villigen.
