Abstract:
I will give a short introduction to interactive theorem proving (using
Lean) and will then discuss what would be needed to a) state and b) give
a proof of Mordell's Conjecture in Lean, building on its mathematical
library Mathlib.