Foundations

Jeremy Avigad

Abstract

This is a draft of a chapter on mathematical logic and foundations for an upcoming handbook of computational proof assistants.

arXiv comments: For the forthcoming Handbook of Proof Assistants and Their Applications in Mathematics and Computer Science, edited by Jasmin Blanchette and Assia Mahboubi
Journal reference
DOI
Subjects: cs.LOLogic in Computer Science math.LOLogic

Linked by 2 identifiable commenters in 2 comments across 2 threads, from Mar 2022 to Nov 2023.

Comments linking this paper, per year.

What do we mean by "the foundations of mathematics"? Nov 20231 comment
- Jeremy Avigad made available a 54-page draft chapter on mathematical logic and foundations [1]. Quoting from the abstract: > The formal foundation of a proof assistant is the formal deductive system with respect to which the correctness of the proof assistant’s implementation is…
  
  trompNov 1, 2023View on HN Parent context
With Category Theory, Mathematics Escapes from Equality (2019) Mar 20221 comment
- I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In the community of computer-aided formalization, a lot of interest in modern type theory arose, because some things in…
  
  anfelorMar 27, 2022View on HN Parent context

Connected through shared HN threads, not inferred similarity or a recommendation.