◍wovepaper
SearchResearchersInstitutions
Sign in
math.AGJan 1, 2021
8
citations (OpenAlex)
authors
  • Kevin Buzzard
  • Chris Hughes
  • Kenny Lau
  • Amelia Livingston
  • Ramon Fernández Mir
  • Scott Morrison
institutions
  • Imperial College London
  • The University of Sydney
  • University of Edinburgh
arXiv abstractPDF
paper

Schemes in Lean

arXiv:2101.02602 · doi:10.1080/10586458.2021.1983489

Abstract

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

10 pages. To appear in Experimental Mathematics

References in corpus (1)

  • The Lean mathematical library

Cited by in corpus (1)

  • Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
◍wovepaper

Papers, researchers and institutions, woven together.

Explore
  • Search
  • Researchers
  • Institutions
Account
  • Library
  • Chat
Data
  • arXiv.org
  • Semantic Scholar
  • OpenAlex
  • Latest RSS
AboutContactPrivacyDevelopersllms.txtopenapi.json
Not affiliated with arXiv. Researcher data from Semantic Scholar (ODC-BY) and OpenAlex.