SU\G(𝔸)/K·U

Abstraction boundaries and spec driven development in pure mathematics

Authors

Johan Commelin, Adam Topaz
Type: Article
Publication Date: 2024-02-15
Citations: 2
DOI: https://doi.org/10.1090/bull/1831

Abstract

In this article we discuss how <italic>abstraction boundaries</italic> 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.

Topics

Locations

  • arXiv (Cornell University)
    View PDF
  • Utrecht University Repository (Utrecht University)
    View PDF
  • Bulletin of the American Mathematical Society
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

Similar Works

Action Title Date Authors
+ PDF Ask
Abstraction boundaries and spec driven development in pure mathematics 2023-01-01 Johan Commelin Adam Topaz
+ PDF Ask
The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems 2020-01-01 Katja BerÄŤiÄŤ Jacques Carette William M. Farmer Michael Kohlhase Dennis MĂĽller Florian Rabe Yasmine Sharoda
+ PDF Ask
The Space of Mathematical Software Systems - A Survey of Paradigmatic Systems. 2020-02-12 Katja BerÄŤiÄŤ Jacques Carette William M. Farmer Michael Kohlhase Dennis MĂĽller Florian Rabe Yasmine Sharoda
+ PDF Ask
Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle 2019-01-01 Jonas Bayer Marco David Abhik Pal Benedikt Stock
+
Reasoning-and-proving opportunities in elementary mathematics textbooks 2013-07-25 Kristen N. Bieda Xueying Ji Justin Drwencke Andrew L. Picard
+
A hands-on approach to proof and abstraction 2010-01-18 Doug Ensley
+ PDF Ask
Formalising Mathematics in Simple Type Theory 2019-01-01 Lawrence C. Paulson
+
On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy 2021-01-01 Angeliki Koutsoukou-Argyraki
+ PDF Ask
Computer Theorem Proving in Mathematics 2004-07-01 Carlos Simpson
+
Generic Proving: Reflections on Scope and Method 2014-12-31 Uri Leron Orit Zaslavsky
+
Formalizing Mathematics using the Lean Theorem Prover. 2016-01-01 Leonardo de Moura
+ PDF Ask
Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started 2020-10-06 Angeliki Koutsoukou-Argyraki
+
Abstraction in mathematics: Conflict, resolution and application 1995-04-01 Michael Mitchelmore Paul J. White
+
Theorem Proving in Elementary Analysis 2007-01-01 Joanna Porter Guild
+ PDF Ask
What Is Wrong with Abstraction?† 2005-06-01 Michael Potter Peter Sullivan
+
Outlines of a Formalist Philosophy of Mathematics 1951-01-01 Haskell B. Curry
+ PDF Ask
Top-down Automated Theorem Proving (Notes for Sir Timothy) 2023-01-01 Craig E. Larson Nico Van Cleemput
+
Exposé Bourbaki 1086 : Developments in formal proofs 2018-11-06 Thomas Hales
+ PDF Ask
Algorithm and abstraction in formal mathematics 2024-05-07 Heather Macbeth
+ PDF Ask
Realms: A Structure for Consolidating Knowledge about Mathematical Theories 2014-01-01 Jacques Carette William M. Farmer Michael Kohlhase

Cited by (1)

Action Title Date Authors
+ PDF Ask
Mathematical reasoning and the computer 2024-02-15 Kevin Buzzard

Citing (3)

Action Title Date Authors
+
Geometric Integration Theory 1957-12-31 Hassler Whitney
+ PDF Ask
A FORMAL PROOF OF THE KEPLER CONJECTURE 2017-01-01 Thomas Hales Mark Adams Gertrud Bauer TAT DAT DANG John Harrison Hoang Le Truong Cezary Kaliszyk Victor Magron Sean McLaughlin TAT THANG NGUYEN
+ PDF Ask
The lean mathematical library 2020-01-20 The mathlib Community