Chaire de Professeur Junior in Lyon: Generative AI for formal proofs

The CNRS (French National Centre for Scientific Research) opens a CPJ (= Chaire de Professeur Junior) this year on the topic “Generative AI for formal proofs”.

This is a tenure-track position. After 3 to 6 years, the person holding the position gets a tenure review and, if they are successful, they become a CNRS senior researcher (with tenure, and with no teaching duties). It is expected that the success rate at tenure reviews will be high, but the positions are very new, and the first tenure reviews have not taken place yet.

The conditions of the position are the following:

  • It is based in Lyon, either at UMPA (the math department of the ENS de Lyon), LIP (the computer science department of the ENS de Lyon) or ICJ (the math department of the Université Lyon 1+Université Saint-Étienne);
  • You need a PhD to apply, and ideally some post-PhD experience;
  • Salary will be around 55 000 euro a year before taxes (depending on experience level);
  • There is a startup package of 200 000 euro.
  • There is teaching, around 45 hours of lecturing a year (or 64 hours of exercise sessions). It’s typically graduate teaching and can be done in English.

The application deadline is September 2 at 17:00 (6 days from now) and the selection process (including interviews) will take place during the fall. The position will start at the end of 2026, with deferrals being possible until February 2027.

If you are interested, you should contact at least one of the three departments: UMPA (https://www.umpa.ens-lyon.fr/), LIP (Home), ICJ (Institut Camille Jordan). Ideally, find people you could be working with and write to them.

Important note about the application website and letters of recommendation.
Here is the information that was recently communicated from the CNRS people managing these positions:

  1. The application website only lets you include very short (4000/6000 characters) summaries of your previous work and research project and doesn’t let you use LaTeX. You can put longer versions with formulas and a bibliography in the pdf file that you will upload as CV. This is actually strongly recommended: use the “CV” as your real application and treat the fields on the application website as summaries. (In applications for the usual CNRS junior positions, the report on previous work and the research project usually take 8-10 pages each, sometimes longer for more experienced candidates.)

  2. Letters of recommendation can be sent directly by their writer to the president of the hiring committee. This is Christophe Besse (christophe.besse@cnrs.fr) for the “AI for formalization” position, and Christophe Delaunay (christophe.delaunay@cnrs.fr) for the “number theory” position. Ask the letter writers to mention in their emails for which person and position they are sending the letter.

If you have further questions about the position and/or the process, you can contact me (Cyril Cohen cyril.cohen@inria.fr) for questions.