Ingénieur Lean, mathématiques formelles (Lean 4, Mathlib, démonstration de théorèmes) (H/F)

À propos du poste

Un laboratoire d'IA de premier plan recherche des ingénieurs Lean, des mathématiciens formels et des ingénieurs de preuves pour aider ses modèles à énoncer et à démontrer correctement des mathématiques. Au-delà de vérifier qu'une preuve compile, le travail consiste à juger si une formalisation traduit réellement l'énoncé visé. L'engagement est à temps partiel, d'au moins 20 heures par semaine, avec une marge de progression jusqu'à 40.

Vos missions

• Écrire des énoncés et des preuves idiomatiques en Lean 4 qui compilent avec la version actuelle de mathlib, en algèbre, analyse, théorie des nombres, combinatoire et logique
• Formaliser des mathématiques en langage naturel, des problèmes de concours aux lemmes de niveau recherche, en vérifiant que la version formelle correspond à l'original
• Relire les productions Lean générées par l'IA, repérer où elles échouent ou démontrent autre chose que ce qui est visé, et fournir des retours écrits précis
• Contribuer à définir des lignes directrices et des grilles d'évaluation sur la qualité des preuves, la fidélité des énoncés et les conventions de mathlib
• Travailler avec d'autres ingénieurs Lean et avec les chercheurs du laboratoire pour maintenir des standards cohérents

Profil recherché

• Expérience concrète de l'écriture de preuves formelles en Lean 4 (contributions à mathlib, projet de formalisation, outil ou bibliothèque Lean, ou travail d'autoformalisation)
• Aisance avec mathlib et les tactiques de Lean 4
• Solide formation en mathématiques fondées sur la preuve, en informatique théorique ou en logique, attestée par un diplôme ou des travaux de recherche
• Disponibilité fiable de 20 heures et plus par semaine en jours ouvrés
• Communication écrite claire
• Un plus : Coq/Rocq, Isabelle, Agda ou Haskell, métaprogrammation Lean, ou expérience en IA pour les mathématiques (prouveurs à base de LLM, miniF2F, ProofNet, PutnamBench)

Rémunération et modalités

• Rémunération : $90-$110 par heure
• Temps partiel, 20 heures par semaine minimum, jusqu'à 40
• À distance, aucune restriction géographique indiquée
• Emploi en W-2 via Cincinnatus LLC (ou une entité internationale appropriée), placé auprès du laboratoire d'IA