Connectionists: 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 <joel at mpi-sws.org
>.

To apply, please send a CV and a research statement by email to <
hr at 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/ <http://people.mpi-sws.org/~joel/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.srv.cs.cmu.edu/pipermail/connectionists/attachments/20260225/121206c7/attachment.html>