A Finitist's Manifesto: Do we need to Reformulate the Foundations of
Mathematics?
- URL: http://arxiv.org/abs/2009.06485v1
- Date: Mon, 14 Sep 2020 14:44:08 GMT
- Title: A Finitist's Manifesto: Do we need to Reformulate the Foundations of
Mathematics?
- Authors: Jonathan Lenchner
- Abstract summary: This essay is a call for practicing mathematicians who have been sleep-walking in their infinitary paradise take heed.
Much of mathematics relies upon (i) the "existence" of objects that contain an infinite number of elements, (ii) our ability, "in theory", to compute with an arbitrary level of precision, or (iii) our ability, "in theory", to compute for an arbitrarily large number of time steps.
- Score: 1.384477926572109
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: There is a problem with the foundations of classical mathematics, and
potentially even with the foundations of computer science, that mathematicians
have by-and-large ignored. This essay is a call for practicing mathematicians
who have been sleep-walking in their infinitary mathematical paradise to take
heed. Much of mathematics relies upon either (i) the "existence'" of objects
that contain an infinite number of elements, (ii) our ability, "in theory", to
compute with an arbitrary level of precision, or (iii) our ability, "in
theory", to compute for an arbitrarily large number of time steps. All of
calculus relies on the notion of a limit. The monumental results of real and
complex analysis rely on a seamless notion of the "continuum" of real numbers,
which extends in the plane to the complex numbers and gives us, among other
things, "rigorous" definitions of continuity, the derivative, various different
integrals, as well as the fundamental theorems of calculus and of algebra --
the former of which says that the derivative and integral can be viewed as
inverse operations, and the latter of which says that every polynomial over
$\mathbb{C}$ has a complex root. This essay is an inquiry into whether there is
any way to assign meaning to the notions of "existence" and "in theory'" in (i)
to (iii) above.
Related papers
- Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning [85.635988711588]
We argue that enhancing the capabilities of large language models requires a paradigm shift in the design of mathematical datasets.
We advocate for mathematical dataset developers to consider the concept of "motivated proof", introduced by G. P'olya in 1949, which can serve as a blueprint for datasets that offer a better proof learning signal.
We provide a questionnaire designed specifically for math datasets that we urge creators to include with their datasets.
arXiv Detail & Related papers (2024-12-19T18:55:17Z) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
We present LeanAgent, a novel lifelong learning framework for formal theorem proving.
LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge.
It successfully proves 155 theorems previously unproved formally by humans across 23 diverse Lean repositories.
arXiv Detail & Related papers (2024-10-08T17:11:24Z) - MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
MathBench is a new benchmark that rigorously assesses the mathematical capabilities of large language models.
MathBench spans a wide range of mathematical disciplines, offering a detailed evaluation of both theoretical understanding and practical problem-solving skills.
arXiv Detail & Related papers (2024-05-20T17:52:29Z) - 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) - MathScale: Scaling Instruction Tuning for Mathematical Reasoning [70.89605383298331]
Large language models (LLMs) have demonstrated remarkable capabilities in problem-solving.
However, their proficiency in solving mathematical problems remains inadequate.
We propose MathScale, a simple and scalable method to create high-quality mathematical reasoning data.
arXiv Detail & Related papers (2024-03-05T11:42:59Z) - Algorithm-assisted discovery of an intrinsic order among mathematical
constants [3.7689882895317037]
We develop a computer algorithm that discovers an unprecedented number of continued fraction formulas for fundamental mathematical constants.
The sheer number of formulas unveils a novel mathematical structure that we call the conservative matrix field.
Such matrix fields unify thousands of existing formulas, generate infinitely many new formulas, and lead to unexpected relations between different mathematical constants.
arXiv Detail & Related papers (2023-08-22T23:27:47Z) - 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) - Peano: Learning Formal Mathematical Reasoning [35.086032962873226]
General mathematical reasoning is computationally undecidable, but humans routinely solve new problems.
We posit that central to both puzzles is the structure of procedural abstractions underlying mathematics.
We explore this idea in a case study on 5 sections of beginning algebra on the Khan Academy platform.
arXiv Detail & Related papers (2022-11-29T01:42:26Z) - Finite mathematics as the most general (fundamental) mathematics [0.0]
Quantum theory based on a finite ring of characteristic $p$ is more general than standard quantum theory because the latter is a degenerate case of the former in the formal limit $ptoinfty$.
arXiv Detail & Related papers (2022-03-09T18:46:57Z) - Noisy Deductive Reasoning: How Humans Construct Math, and How Math
Constructs Universes [0.5874142059884521]
We present a computational model of mathematical reasoning according to which mathematics is a fundamentally process.
We show that this framework gives a compelling account of several aspects of mathematical practice.
arXiv Detail & Related papers (2020-10-28T19:43:14Z)
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.