Generative AI and Formal Proofs M/F
- Tenure Track Position
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
CNRS Mathématiques
Contract Type
Tenure Track Position
Working hHours
Full Time
Remuneration
Annual salary from 54 600 Euros to 57 800 Euros depending on professionnal experience.
Apply Application Deadline : 02 September 2026 17:00
Job Description
Summary of the scientific project
Proof assistants (Rocq/Coq, Lean) make it possible to certify mathematical results with absolute rigor. Milestones such as Gonthier's proof of the four-color theorem illustrate their power. Their historical limitation lies in the considerable human effort required to translate a mathematical proof into a formal script, thereby hindering scalability.
Recent progress in generative AI is changing the landscape: models trained on corpora of formal proofs can now generate and explore proofs in a largely autonomous manner. A decisive advantage of this paradigm is the intrinsic verifiability of the proofs produced - their validity is mechanically certified, without external expertise, thereby removing the usual doubts about the reliability of AI outputs.
Developing effective models for this task requires expertise at the intersection of proof assistants, language-model architectures, and mathematics.
Summary of the teaching project
The teaching project will be discussed with the site.
Potential host facilities
- INSMI - CNRS Mathématiques
- ICJ - Institut Camille Jordan
- LIP - Laboratoire de l'informatique du parallélisme
- UMPA - Unité de Mathématiques Pures et Appliquées
Your Profil
Profile Required
Holders of a doctorate or a PhD or equivalent degree or applicants who have gained scientific qualifications or carried out scientific work deemed to be of an equivalent level.There is no restriction on the age or nationality of applicants. All CNRS positions are accessible to people with disabilities, with special arrangements for tests made necessary by the nature of the disability
Your Work Environment
Host Lab Strategy
For this CPJ, we are targeting the Lyon ecosystem, which is particularly interested in proof theory in both mathematics and computer science. LIP, and more specifically the PLUME team, together with ICJ, are at the heart of these issues in formal verification and will be natural hosts for the CPJ.
Institution Strategy
LLM-based generative AI is profoundly reshaping the topic of formal proofs at the interface between Mathematics and Computer Science. Its ability to generate proofs in the sense of proof theory is becoming more robust, even though it remains fragile. Recent work, particularly for example in Lean, shows that momentum is building and that this is a topic that must be addressed strategically in order to tackle new and highly interdisciplinary scientific challenges in this field.
One of the axes of the CNRS COMP concerns generative AI for science. This Junior Professor Chair is fully aligned with this initiative. It will enable the CNRS to position itself in a high-potential and crucial field concerning the evolution of research in mathematics.
International Strategy
CNRS widely welcomes and recruits researchers internationally. More than 30% of those recruited come from abroad. This recruitment will have the same ambition.
Compensation and benefits
Compensation
Annual salary from 54 600 Euros to 57 800 Euros depending on professionnal experience.
Total funding
200k€
Annual leave and RTT
44 jours
Remote Working practice and compensation
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
Research Policy
Open Science
The CNRS is developing a strong policy in favor of open science. Open science consists of making research results "as accessible as possible and closed as necessary". As such, the CNRS aims to make 100% of the texts of publications resulting from the work of its laboratories accessible , in particular through deposit in HAL. The data produced must also be made available and reusable, except for specific restrictions. In addition, the guiding principles of individual evaluation have been revised in accordance with the DORA declaration, to be more qualitative and to take into account all facets of the researcher's profession.
Science and society
The relationship between science and society is now recognized as a full dimension of scientific activity. The project will develop this dimension in synergy with all the partners. The resulting research work will contribute to informing public decision-making. Participatory science initiatives may be initiated with actors from the project’s socio-economic and cultural eco-system.
Scientific dissemination
The dissemination of the results will be done through world-class scientific productions: publications, patents, software... In addition, the results will be communicated to various targets such as scientific communities, media, decision makers, general public, schools, etc., with an adapted calendar. Specific tools may be developed such as websites, newsletters, meetings, international symposia, summer schools and conferences.
About the offer
| Offer reference | CPJ-2026-036 |
|---|---|
| CN Section(s) / Research Area | Mathematics and mathematical interactions Information sciences: bases of information technology, calculations, algorithms, representations, uses |
About the CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.