This repository hosts the development of a formalisation of algebraic schemes and Nagata's Conjecture on plane algebraic curves based on Homotopy Type Theory and using topoi as models of first-order languages. For motivation, mathematical details and interesting observations on the formalisation look at HoTT-Case-Study.

The project started in Lean 2 using the extensive HoTT library of van Doorn, von Raumer and Buchholtz. Note that the frozen version of Lean 2 can still be installed and works well in the HoTT mode. Unfortunately, for intrinsic logical reasons this library could only be ported to Lean 3 using some tricks, so for comparison reasons I stored the Lean 2 files into a separate folder Lean2-HoTT.

At the moment, formalisation is done in the HOTT3 library based on Lean 3. Look in the overview file to see which files compile at the moment, which still have sorries or must be completely revised. Of course, the next step must be to port it to Lean 4. However, before starting this process it may be worth thinking hard on a redesign of HoTT3, possibly including developments from Cubical Type Theory that make the Univalence Axiom and Higher Inductive Types into computable theorems and constructions. Theoretically, this is proven to work (see the paper of Cohen, Coquand, Huber and Mörtberg for details), but there is no interpretation of Cubical Type Theory implemented in a Homotopy Type Theory using the Calculus of Inductive Construction, like HoTT 3.