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

DOI10.1080/10586458.2022.2062073MaRDI QIDQ5094472zbMATH OpenOpenAlexFDO

Authors Anthony Bordg, Wenda Li, Lawrence C. Paulson

Publication date 3 August 2022

Published in Experimental Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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

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)

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.

Recommendations

• Schemes in Lean
• Mathematical Knowledge Management
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cites work

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

Cited in

(7)

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

Describes a project that uses

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)