Post #1471885
2023-10-03 17:08 UTC
@xenaproject This might be a dumb question (albeit one that I'm unlikely to be alone in asking), but what's the current state of the art in formalized arithmetic geometry?
Replies (1)
-
@xenaproject@mathstodon.xyz 2023-10-06 12:49
@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: