PhD positions

Proof assistants like Coq or Lean are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are difficult to reuse. In this thesis, we propose to design and implement new tools to improve the robustness, the inter-operability and the reuse of formal proof developments. We hope this will make proving new results formally easier.

Foundations of Mathematics
Logic and Type Theory
Applications are possible in various fields of mathematics including combinatorics, algebraic and/or differential geometry and applied mathematics.

Our research aims to establish a correspondence between continuous and discrete representations of objects, crucial for geometric operations in image processing. To achieve this, the thesis objective is to extend the class of Curves with Locally Bounded Total Curvature developed in 2D to 3D. This study involves establishing local topological properties on surfaces to demonstrate results on the topology of their discretization and subsequently comparing the global geometric quantities of the continuous surface with its discretization in 3D.

Bachelor level in geometry and topology.
Programming skill useful but not required.