Strange new universes: Proof assistants and synthetic foundations

DOI10.1090/bull/1830OpenAlexW4391839087MaRDI QIDQ6130525

Michael Shulman

Publication date: 3 April 2024

Published in: Bulletin of the American Mathematical Society (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1090/bull/1830

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• The simplicial model of univalent foundations (after Voevodsky)
• Idempotents in intensional type theory
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Modalities and Parametric Adjoints
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Strange new universes: Proof assistants and synthetic foundations