Appears in collection : Workshop Schlumberger : Types dépendants et Formalisation des mathématiques

What can be done when formalising mathematics without dependent types? I will give you new insights into this question by exploring the capability and possible limitations of the Isabelle/HOL proof assistant. I will explain what we learnt formalising Grothendieck's schemes using only Isabelle's module system called "locales".