Home

Welcome to my webpage!

I'm a researcher at Huawei's Lagrange Centre in Paris.

Some of my scientific/tech interests:

• computerisation of mathematics and computer-assisted proofs (mainly in Lean 4 these days)

• AI and ML for reasoning and theorem proving 

• explainable and trustworthy AI, through the lens of formal verification

• structured AI 

• AI-powered math tools 

• metaprogramming in Lean 4

• type theory and programming languages

• Homotopy Type Theory/Univalent Foundations

• interoperability between formal proof systems

• quantum computing and information

• (higher) category theory and (abstract) homotopy theory

• mathematical study of type theories