PulseExploreJournal ClubDebatesTrendingResearchersJournals
Instagram
HomeExploreJournal ClubTrending
Synapse
⌘+K
Synapse
February 15, 2024Bulletin of the American Mathematical Society15 citationsOpen Access

Mathematics and the formal turn

View Full Paper
JAJeremy Avigad

Key Points

  • Mathematical definitions and proofs can be represented in formal systems, facilitating precise communication.
  • Computational proof assistants enable the encoding of complex mathematical knowledge in digital form.
  • Formal systems utilize precise grammars and rules of use for effective mathematical representation and proof construction. Potential advancements hinge on these technologies, suggesting they may reshape mathematical practice.

Abstract

Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can help us do mathematics.

Ask AI
Helpful
Bookmark
Share
View Full Paper

Cite This Study

Jeremy Avigad (2024) studied this question.

synapsesocial.com/papers/68e78f6db6db6435877013aahttps://doi.org/10.1090/bull/1832
Ask AI
Helpful
Bookmark
Share
View Full Paper

Also Consider

Synapse has enriched 4 closely related papers on similar clinical questions. Consider them for comparative context:

  1. 1Notices of the American Mathematical Society2012 · 1,342 citations
  2. 2Artificial Intelligence to Assist Mathematical Reasoning2023 · 1 citations
  3. 3The Resolution of Keller’s Conjecture2020 · 29 citations
  4. 4The science of brute force2017 · 96 citations