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

Anthony Bordg; Lawrence Paulson; Wenda Li

REVIEW

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2104.09366 v3 pith:BDPMU2DJ submitted 2021-04-19 math.AG cs.LOmath.LO

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

Anthony Bordg , Lawrence Paulson , Wenda Li This is my paper

classification math.AG cs.LOmath.LO

keywords schemessimpletheorytypedependentgrothendieckmathematicalparticular

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original abstract

Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the simple type theory of the proof assistant Isabelle/HOL, and we discuss the design choices which make this work possible. We show in the particular case of schemes how the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales.

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

discussion (0)