'Hello world' project in Lean.
This is a work in progress - currently I'm proving equivalences between different definitions for what it means for an integral domain to be integrally closed.
The next step would be to implement Neukirch's definition of a Dedekind domain: an integral domain that is Noetherian, integrally closed, and in which every nonzero prime ideal is maximal.