Roelof Oosterhuis (Groningen): Another step in formalizing Fermat's Last Theorem
My master's thesis involves a project in mechanized theorem
proving. Starting from scratch I tried to formally prove the cases n=4
and n=3 of Fermat's Last Theorem. One motivation for this research is
the list of 'ten challenging research problems in computer science' from
Jan Bergstra, leaded by: "Formalize and verify by computer a proof of
Fermat's Last Theorem."
In my talk I will give an impression of what it is like for a
mathematician to get started with proof assistants, with a special focus
on number theory in 'Isabelle'.