Abstraction boundaries and spec driven development in pure mathematics

DOI10.1090/bull/1831arXiv2309.14870OpenAlexW4391839082MaRDI QIDQ6130524

Johan Commelin, Adam Topaz

Publication date: 3 April 2024

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

Full work available at URL: https://arxiv.org/abs/2309.14870

Mathematics Subject Classification ID

Methodology of mathematics (00A35) Formalization of mathematics in connection with theorem provers (68V20) Mathematical knowledge management (68V30)

Cites Work

• Unnamed Item
• How to write mathematics
• Correction to: ``On topological cyclic homology
• The Lean Theorem Prover (System Description)
• Liquid Tensor Experiment
• A FORMAL PROOF OF THE KEPLER CONJECTURE

This page was built for publication: Abstraction boundaries and spec driven development in pure mathematics