Abstraction boundaries and spec driven development in pure mathematics

• URL: http://arxiv.org/abs/2309.14870v1
• Date: Tue, 26 Sep 2023 11:59:32 GMT
• Title: Abstraction boundaries and spec driven development in pure mathematics
• Authors: Johan Commelin and Adam Topaz
• Abstract summary: In this article we discuss how abstraction boundaries can help tame complexity in mathematical research. We argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• A Concise Mathematical Description of Active Inference in Discrete Time [0.0]
  The main part of the paper serves as a basic introduction to the topic, including a detailed example illustrating the theory on action selection. In the appendix the more subtle mathematical details are discussed. This part is aimed at readers who have already studied the active inference literature but struggle to make sense of the mathematical details and derivations.
  arXiv  Detail & Related papers  (2024-06-11T21:09:45Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  The current state-of-the-art in artificial intelligence is impressive, especially in terms of mastery of language, but not so much in terms of mathematical reasoning. This essay builds on the idea that current deep learning mostly succeeds at system 1 abilities. It takes an information-theoretical posture to ask questions about what constitutes an interesting mathematical statement.
  arXiv  Detail & Related papers  (2024-03-07T15:12:06Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  This work investigates the applicability of large language models (LLMs) in formalizing advanced mathematical concepts. We envision an automated process, called emphmath-PVS, to extract and formalize mathematical theorems from research papers.
  arXiv  Detail & Related papers  (2023-10-25T23:54:04Z)
• Parmesan: mathematical concept extraction for education [0.5520082338220947]
  We develop a prototype system for searching for and defining mathematical concepts in context, focusing on the field of category theory. This system depends on natural language processing components including concept extraction, relation extraction, definition extraction, and entity linking. We also provide two cleaned mathematical corpora that power the prototype system, which are based on journal articles and wiki pages.
  arXiv  Detail & Related papers  (2023-07-13T11:55:03Z)
• Towards a Holistic Understanding of Mathematical Questions with Contrastive Pre-training [65.10741459705739]
  We propose a novel contrastive pre-training approach for mathematical question representations, namely QuesCo. We first design two-level question augmentations, including content-level and structure-level, which generate literally diverse question pairs with similar purposes. Then, to fully exploit hierarchical information of knowledge concepts, we propose a knowledge hierarchy-aware rank strategy.
  arXiv  Detail & Related papers  (2023-01-18T14:23:29Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  We review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade. Recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning.
  arXiv  Detail & Related papers  (2022-12-20T18:46:16Z)
• Open Geometry Prover Community Project [0.0]
  The Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common "umbrella" This article describes the necessary steps to such integration and the current implementation of some of those steps.
  arXiv  Detail & Related papers  (2022-01-03T09:27:23Z)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
  arXiv  Detail & Related papers  (2021-10-18T10:45:59Z)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  We develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources. We benchmark strong neural methods on mathematical reference retrieval and generation tasks.
  arXiv  Detail & Related papers  (2021-03-24T03:14:48Z)
• Explaining Creative Artifacts [69.86890599471202]
  We develop an inverse problem formulation to deconstruct the products of and compositional creativity into associative chains. In particular, our formulation is structured as solving a traveling salesman problem through a knowledge graph of associative elements.
  arXiv  Detail & Related papers  (2020-10-14T14:32:38Z)
• Information-Theoretic Abstractions for Planning in Agents with Computational Constraints [16.565205172451662]
  We show how a path-planning problem in an environment can be systematically approximated by solving a sequence of easier to solve problems on abstractions of the original space. A numerical example is presented to show the utility of the approach and to corroborate the theoretical findings.
  arXiv  Detail & Related papers  (2020-05-19T17:32:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.