Simple type theory is not too simple: Grothendieck's schemes without dependent types

DOI10.1080/10586458.2022.2062073zbMATH Open1498.14001arXiv2104.09366OpenAlexW3156224329MaRDI QIDQ5094472FDOQ5094472

Authors: Anthony Bordg, Wenda Li, Lawrence C. Paulson 

Publication date: 3 August 2022

Published in: Experimental Mathematics (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2104.09366

Recommendations

• Schemes in Lean
• Mathematical Knowledge Management
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Formalization of the fundamental group in untyped set theory using auto2
• Formalization of the fundamental group in untyped set theory using auto2

zbMATH Keywords

type theorysheavesschemeshigher order logiclogic and verification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Schemes and morphisms (14A15) Software, source code, etc. for problems pertaining to algebraic geometry (14-04) Research data for problems pertaining to algebraic geometry (14-11)

Cites Work

• Coquelicot: a user-friendly library of real analysis for Coq
• The Lean theorem prover (system description)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Type classes and filters for mathematical analysis in Isabelle/HOL
• A formulation of the simple theory of types
• Locales: a module system for mathematical theories
• A machine-checked proof of the odd order theorem
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• From types to sets by local type definition in higher-order logic
• Exploring the structure of an algebra text with locales
• Algebraically Closed Fields in Isabelle/HOL
• Schemes in Lean

Cited In (7)

• Graded rings in Lean's dependent type theory
• Schemes in Lean
• Formalising Mathematics in Simple Type Theory
• Type classes and filters for mathematical analysis in Isabelle/HOL
• A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
• Title not available (Why is that?)
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

Uses Software

• Coq
• Isabelle/HOL
• Coquelicot
• Locales
• Lean

This page was built for publication: Simple type theory is not too simple: Grothendieck's schemes without dependent types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094472)