The reviewed record of science sign in
Pith

arxiv: 2101.02602 · v2 · pith:WOTKNTJF · submitted 2021-01-07 · math.AG

Schemes in Lean

Kevin Buzzard , Chris Hughes , Kenny Lau , Amelia Livingston , Ramon Fern\'andez Mir , Scott Morrison This is my paper

Reviewed by Pithpith:WOTKNTJFopen to challenge →

classification math.AG
keywords leanschemesdifferentformalisedproverstorytelltheorem
0
0 comments X
read the original abstract

We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.