The Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany, is inviting applications for a postdoctoral position in proof automation and automated reasoning, with a research focus on LEAN, computer algebra, discrete dynamical systems, automated verification, number theory, symbolic computation, and theoretical computer science. The position is based in the group of Prof. Joël Ouaknine and is a joint collaboration with Prof. Laura Kovács at TU Wien, Austria. The project aims to advance the state of the art in formalising and proving mathematical theorems using LEAN, leveraging AI tools (especially large language models) for mathematical proof generation, and contributing to research areas such as logic in computer science, formal verification, automata theory, programming language theory, probabilistic models, cybersecurity, learning, randomised algorithms, concurrency theory, and program synthesis.

Applicants should hold or be near completion of a PhD in Computer Science, Mathematics, or a closely related discipline, with excellent academic records. Candidates must demonstrate expertise in formalising and proving mathematical theorems with LEAN, experience with AI tools for mathematical proofs, and a strong publication record in relevant areas. Additional desired qualities include high personal responsibility, initiative, willingness to travel for conferences, ability to work independently and in interdisciplinary contexts, a team-oriented mindset, interest in mentoring students and research assistants, and proficiency in English.

The position is full-time (39 hours/week) for two years initially, with the possibility of renewal. Salary is according to TVöD / Bund EG 14, commensurate with experience and qualifications, and based on university and ERC funding guidelines. The post is fully funded and 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, welcoming applications from all backgrounds, especially women and minorities underrepresented in computer science.

To apply, candidates should send a CV and research statement by email to [email protected] with the reference (LEAN-2026) in the subject line by 15 March 2026. Informal enquiries can be directed to Prof. Joël Ouaknine at [email protected]. Interviews are expected to 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 official position page or the LinkedIn announcement.

Keywords: proof automation, automated reasoning, LEAN, computer algebra, discrete dynamical systems, automated verification, number theory, symbolic computation, theoretical computer science, formal methods, Max Planck Institute for Software Systems, TU Wien.