Unsupervised Discovery of Formulas for Mathematical Constants

• URL: http://arxiv.org/abs/2412.16818v1
• Date: Sun, 22 Dec 2024 01:43:56 GMT
• Title: Unsupervised Discovery of Formulas for Mathematical Constants
• Authors: Michael Shalyt, Uri Seligmann, Itay Beit Halachmi, Ofir David, Rotem Elimelech, Ido Kaminer,
• Abstract summary: We propose a systematic methodology for categorization, characterization, and pattern identification of such formulas.<n>Key to our methodology is introducing metrics based on the convergence dynamics of the formulas, rather than on the numerical value of the formula.<n>We test our methodology on a set of 1,768,900 such formulas, identifying many known formulas for mathematical constants, and discover previously unknown formulas for $pi$, $ln(2)$, Gauss', and Lemniscate's constants.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Ongoing efforts that span over decades show a rise of AI methods for accelerating scientific discovery, yet accelerating discovery in mathematics remains a persistent challenge for AI. Specifically, AI methods were not effective in creation of formulas for mathematical constants because each such formula must be correct for infinite digits of precision, with "near-true" formulas providing no insight toward the correct ones. Consequently, formula discovery lacks a clear distance metric needed to guide automated discovery in this realm. In this work, we propose a systematic methodology for categorization, characterization, and pattern identification of such formulas. The key to our methodology is introducing metrics based on the convergence dynamics of the formulas, rather than on the numerical value of the formula. These metrics enable the first automated clustering of mathematical formulas. We demonstrate this methodology on Polynomial Continued Fraction formulas, which are ubiquitous in their intrinsic connections to mathematical constants, and generalize many mathematical functions and structures. We test our methodology on a set of 1,768,900 such formulas, identifying many known formulas for mathematical constants, and discover previously unknown formulas for $\pi$, $\ln(2)$, Gauss', and Lemniscate's constants. The uncovered patterns enable a direct generalization of individual formulas to infinite families, unveiling rich mathematical structures. This success paves the way towards a generative model that creates formulas fulfilling specified mathematical properties, accelerating the rate of discovery of useful formulas.

Related papers

• From Euler to AI: Unifying Formulas for Mathematical Constants [0.0]
  We propose a systematic methodology for discovering and proving formula equivalences. A third of the validated formulas for $pi$ were proven to be derivable from a single mathematical object. This work lays a foundation for AI-driven discoveries of connections across scientific domains.
  arXiv  Detail & Related papers  (2025-02-24T14:42:48Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  We advocate for formal mathematical reasoning and argue that it is indispensable for advancing AI4Math to the next level.<n>We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success.
  arXiv  Detail & Related papers  (2024-12-20T17:19:24Z)
• The Ramanujan Library -- Automated Discovery on the Hypergraph of Integer Relations [0.0]
  We present the first library dedicated to mathematical constants and their interrelations.<n>The library is based on a new representation that we propose for organizing the formulas of mathematical constants.<n>During its development and testing, our strategy led to the discovery of 75 previously unknown connections between constants.
  arXiv  Detail & Related papers  (2024-12-16T21:18:44Z)
• 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 generates formal proofs for 155 theorems across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• 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)
• Towards true discovery of the differential equations [57.089645396998506]
  Differential equation discovery is a machine learning subfield used to develop interpretable models. This paper explores the prerequisites and tools for independent equation discovery without expert input.
  arXiv  Detail & Related papers  (2023-08-09T12:03:12Z)
• Automated Search for Conjectures on Mathematical Constants using Analysis of Integer Sequences [0.0]
  Formulas involving fundamental mathematical constants had a great impact on various fields of science and mathematics. Recent efforts to automate the discovery of formulas for mathematical constants, such as the Ramanujan Machine project, relied on exhaustive search. Here we propose a fundamentally different method to search for conjectures on mathematical constants: through analysis of integer sequences.
  arXiv  Detail & Related papers  (2022-12-13T18:01:21Z)
• 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)
• Bayesian Quadrature on Riemannian Data Manifolds [79.71142807798284]
  A principled way to model nonlinear geometric structure inherent in data is provided. However, these operations are typically computationally demanding. In particular, we focus on Bayesian quadrature (BQ) to numerically compute integrals over normal laws. We show that by leveraging both prior knowledge and an active exploration scheme, BQ significantly reduces the number of required evaluations.
  arXiv  Detail & Related papers  (2021-02-12T17:38:04Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50: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.