Skip to Main Content

Bulletin of the American Mathematical Society

The Bulletin publishes expository articles on contemporary mathematical research, written in a way that gives insight to mathematicians who may not be experts in the particular topic. The Bulletin also publishes reviews of selected books in mathematics and short articles in the Mathematical Perspectives section, both by invitation only.

ISSN 1088-9485 (online) ISSN 0273-0979 (print)

The 2024 MCQ for Bulletin of the American Mathematical Society is 0.84.

What is MCQ? The Mathematical Citation Quotient (MCQ) measures journal impact by looking at citations over a five-year period. Subscribers to MathSciNet may click through for more detailed information.

 

Abstraction boundaries and spec driven development in pure mathematics
HTML articles powered by AMS MathViewer

by Johan Commelin and Adam Topaz;
Bull. Amer. Math. Soc. 61 (2024), 241-255
DOI: https://doi.org/10.1090/bull/1831
Published electronically: February 15, 2024

Abstract:

In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.
References
Similar Articles
  • Retrieve articles in Bulletin of the American Mathematical Society with MSC (2020): 68V30, 68V20, 00A35
  • Retrieve articles in all journals with MSC (2020): 68V30, 68V20, 00A35
Bibliographic Information
  • Johan Commelin
  • Affiliation: Mathematisch Institut, Utrecht University, Budapestlaan 6, 3584CD Utrecht, Nederland
  • MR Author ID: 1198615
  • Email: j.m.commelin@uu.nl
  • Adam Topaz
  • Affiliation: Department of Mathematical and Statistical Sciences, University of Alberta, 632 Central Academic Building, Edmonton AB T6G 2G1, Canada
  • MR Author ID: 1051144
  • Email: topaz@ualberta.ca
  • Received by editor(s): July 31, 2023
  • Published electronically: February 15, 2024
  • Additional Notes: The first author was supported by the Deutsche Forschungsgemeinschaft (DFG) grant CO 2587/1-1.
    The second author was supported by NSERC discovery grant RGPIN-2019-04762.
  • © Copyright 2024 by the authors
  • Journal: Bull. Amer. Math. Soc. 61 (2024), 241-255
  • MSC (2020): Primary 68V30, 68V20, 00A35
  • DOI: https://doi.org/10.1090/bull/1831
  • MathSciNet review: 4726990