Schemes in Lean
File(s)Schemes in Lean.pdf (1.2 MB)
Published version
Author(s)
Type
Journal Article
Abstract
We tell the story of how schemes were formalized in three different ways in the Lean theorem prover.
Date Issued
2021-11-23
Date Acceptance
2021-11-01
Citation
Experimental Mathematics, 2021, 31 (2), pp.355-363
ISSN
1058-6458
Publisher
Taylor and Francis Group
Start Page
355
End Page
363
Journal / Book Title
Experimental Mathematics
Volume
31
Issue
2
Copyright Statement
© 2021 The Author(s). Published with license by Taylor & Francis Group, LLC
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
License URL
Identifier
https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000722517700001&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=a2bf6146997ec60c407a63945d4e92bb
Subjects
Science & Technology
Physical Sciences
Mathematics
Scheme
lean
formal proof
Publication Status
Published
Date Publish Online
2021-11-25