Post #1471886

@zwarich I think it's basically "what Lean has", plus "definition of a scheme in Isabelle and in Agda". What Lean has is really very little: sheaves, schemes, open and closed immersions, not too much more. Associativity of the group law for long Weierstrass form elliptic curves over an arbitrary field (incl char 2,3). Take a look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/Scheme.html#AlgebraicGeometry.Scheme to see the kind of things we have. In the directory structure on the left it currently looks like this: