The Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany, in collaboration with TU Wien, is offering a postdoctoral position in proof automation and theoretical computer science. The research will be supervised by Prof. Joël Ouaknine (MPI-SWS) and Prof. Laura Kovács (TU Wien), focusing on areas such as proof automation, automated reasoning, formal methods, computer algebra, discrete dynamical systems, symbolic computation, number theory, and automated verification. The project emphasizes formalising and proving mathematical theorems with LEAN and leveraging AI tools, especially large language models, for mathematical proofs.

Applicants should have a PhD (awarded or nearing completion) in Computer Science, Mathematics, or a closely related field, with excellent grades. Required skills include expertise in LEAN, experience with AI tools for proof generation, and a strong background in logic in computer science, formal verification, automata theory, programming language theory, probabilistic models, cybersecurity, learning, randomised algorithms, concurrency theory, and program synthesis. Candidates should be highly responsible, proactive, willing to travel for conferences, able to work independently and in interdisciplinary contexts, and interested in mentoring students. Proficiency in English is essential.

The position is fully funded for two years (with possible renewal), full-time (39 hours/week), with salary according to TVöD / Bund EG 14, based on experience and qualifications. The role offers a stimulating academic environment within the Saarland Informatics Campus, flexible and family-friendly working arrangements, and opportunities for extended research stays in Vienna. The MPI-SWS and Saarland Informatics Campus actively promote equality and diversity, encouraging applications from underrepresented groups.

The application deadline is 15 March 2026. To apply, send a CV and research statement by email to [email protected] with the reference 'LEAN-2026' in the subject line. For informal enquiries, contact Prof. Joël Ouaknine at [email protected]. Interviews will be held via videoconferencing in the week commencing 30 March 2026, and the starting date is on or after 1 May 2026 by mutual agreement.

For more information, visit the academic pages of Prof. Joël Ouaknine and Prof. Laura Kovács, or the MPI-SWS Automated Program Reasoning Group.