Postdoc in proof automation (LEAN) and theoretical CS / mathematics at MPI-SWS / TU Wien

[Joël Ouaknine]

We are advertising a postdoc position in proof automation and automated reasoning (with expertise in LEAN) at the Max Planck Institute for Software Systems in Saarbrücken, Germany, in the group of Prof. Joël Ouaknine. The project is a joint collaboration with Prof. Laura Kovács at TU Wien.

Research focus:
Broad thematics include: computer algebra, discrete dynamical systems, automated verification, number theory, symbolic computation, and automated reasoning.

We are looking for someone with:
Expertise in formalising and proving mathematical theorems with LEAN,
Experience with interacting and leveraging AI tools (esp. LLMs) in generating mathematical proofs,
Strong background knowledge on -- and preferably publications in -- some of the broad thematics mentioned above.

For informal enquiries, please contact Prof. Joël Ouaknine <jo...@mpi-sws.org>.

To apply, please send a CV and a research statement by email to <h...@mpi-klsb.mpg.de> using the reference (LEAN-2026) in the email subject line, by the deadline of 15 March 2026.

More information available at:
https://people.mpi-sws.org/~joel/positions/LEAN-postdoc.html

--

Joël Ouaknine

Max Planck Institute for Software Systems

Saarland Informatics Campus, Germany

http://mpi-sws.org/~joel/