En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)
Portail > Offres > Offre UMR8243-JEMSAM0-021 - [H/F] Postoctorant - Développement d’outils d’assistance automatisée pour la formalisation mathématique

[M/F] Postdoctoral Researcher Developing Automated Tools to Support Mathematical Formalization

This offer is available in the following languages:
- Français-- Anglais

Date Limite Candidature : vendredi 1 août 2025 23:59:00 heure de Paris

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler

Informations générales

Intitulé de l'offre : [M/F] Postdoctoral Researcher Developing Automated Tools to Support Mathematical Formalization (H/F)
Référence : UMR8243-JEMSAM0-021
Nombre de Postes : 1
Lieu de travail : PARIS 13
Date de publication : vendredi 11 juillet 2025
Type de contrat : Chercheur en contrat CDD
Durée du contrat : 12 mois
Date d'embauche prévue : 1 septembre 2025
Quotité de travail : Complet
Rémunération : Starting at €2,991.58 per month
Niveau d'études souhaité : Doctorat
Expérience souhaitée : Indifférent
Section(s) CN : 06 - Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations

Missions

The aim is to develop a formal and algorithmic framework that supports modular reasoning, regardless of the specific logical or algebraic presentation of concepts and definitions.

Activités

Development of a conceptual and algorithmic framework for formalized mathematics;
scientific writing and dissemination of knowledge;
coordination and interdisciplinary communication between mathematics, computer science, and linguistics.

Compétences

• Expert in operadic and homotopical algebra
• Expert in category theory and higher categories
• Solid knowledge of type theory and categorical logic
• Experience in formalizing mathematics in a type-theory-based system such as Agda, Lean, or Rocq
• Experience in natural language processing (NLP) for the semantic modeling of concepts from linguistic data

Contexte de travail

The position is part of a project aimed at developing a new generation of proof assistants, integrating a linguistic layer and automated assistance tools into their core. These tools are designed to guide researchers and facilitate the construction of certified mathematical documents—from the selection of concepts and definitions to the formulation of theorems and proofs.

Contraintes et risques

No constraints and no risks