Contrats Doctoraux

Les assistants de preuve comme Coq ou Lean deviennent des outils usuels pour faire des mathématiques, mais les développements informatiques associés sont encore très techniques et difficiles à réutiliser. L’objectif de cette thèse est de proposer des outils pour renforcer la robustesse, l’inter-opérabilité et la réutilisabilité de telles preuves formelles, avec pour objectif de faciliter l’émergence de nouveaux résultats prouvés formellement.

Fondements des mathématiques
Logique et théorie des types
Des applications sont possibles dans de nombreux domaines des mathématiques, notamment en combinatoire, en géométrie algébrique et/ou différentielle ainsi qu’en mathématiques appliquées.

Notre recherche vise à établir une correspondance entre les représentations continues et discrètes des objets, crucial pour les opérations géométriques en traitement d'images. Dans ce but, l’objet de la thèse est d’étendre la classe des courbes à Courbure Totale Localement Bornée que nous avons développée en 2D, à la 3D. Cette étude implique d’établir de propriétés topologiques locales sur les surfaces afin de démontrer des résultats sur la topologie de leur discrétisation et, ensuite, de comparer les quantités géométriques globales de la surface continue et de sa discrétisation en 3D.

Niveau licence en géométrie et topologie.
Connaissance en programmation utile mais non requise.