From Euler to AI: Unifying Formulas for Mathematical Constants

• URL: http://arxiv.org/abs/2502.17533v2
• Date: Mon, 16 Jun 2025 13:07:26 GMT
• Title: From Euler to AI: Unifying Formulas for Mathematical Constants
• Authors: Tomer Raz, Michael Shalyt, Elyasheev Leibtag, Rotem Kalisch, Shachar Weinbaum, Yaron Hadad, Ido Kaminer,
• Abstract summary: We present a systematic unification of mathematical formulas.<n>We validate 407 distinct formulas for $pi$ and prove between $pi$ infinite sums.<n>Our method generalizes to other constants, including $zeta(3)$, and unifies knowledge across domains.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The constant $\pi$ has fascinated scholars throughout the centuries, inspiring numerous formulas for its evaluation, such as infinite sums and continued fractions. Despite their individual significance, many of the underlying connections among formulas remain unknown, missing unifying theories that could unveil deeper understanding. The absence of a unifying theory reflects a broader challenge across math and science: knowledge is typically accumulated through isolated discoveries, while deeper connections often remain hidden. In this work, we present an automated framework for the unification of mathematical formulas. Our system combines large language models (LLMs) for systematic formula harvesting, an LLM-code feedback loop for validation, and a novel symbolic algorithm for clustering and eventual unification. We demonstrate this methodology on the hallmark case of $\pi$, an ideal testing ground for symbolic unification. Applying this approach to 455,050 arXiv papers, we validate 407 distinct formulas for $\pi$ and prove relations between 381 (94%) of them, of which 188 (46%) can be derived from a single mathematical object$\unicode{x2014}$linking canonical formulas by Euler, Gauss, Brouncker, and newer ones from algorithmic discoveries by the Ramanujan Machine. Our method generalizes to other constants, including $e$, $\zeta(3)$, and Catalan's constant, demonstrating the potential of AI-assisted mathematics to uncover hidden structures and unify knowledge across domains.

Related papers

• Unsupervised Discovery of Formulas for Mathematical Constants [0.0]
  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.
  arXiv  Detail & Related papers  (2024-12-22T01:43:56Z)
• 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. The library is based on a new representation that we propose for organizing the formulas of mathematical constants. 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)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  We introduce a novel approach for traversing the problem space using task decompositions.<n>We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code.<n>Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• 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)
• 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)
• Automated Discovery of Integral with Deep Learning [0.0]
  We show that deep learning models can approach the task of inferring integrals either through a sequence-to-sequence model, or by uncovering the rudimentary principles of integration. Our experiments show that deep learning models can approach the task of inferring integrals either through a sequence-to-sequence model, or by uncovering the rudimentary principles of integration.
  arXiv  Detail & Related papers  (2024-02-28T04:34:15Z)
• Tempered Calculus for ML: Application to Hyperbolic Model Embedding [70.61101116794549]
  Most mathematical distortions used in ML are fundamentally integral in nature. In this paper, we unveil a grounded theory and tools which can help improve these distortions to better cope with ML requirements. We show how to apply it to a problem that has recently gained traction in ML: hyperbolic embeddings with a "cheap" and accurate encoding along the hyperbolic vsean scale.
  arXiv  Detail & Related papers  (2024-02-06T17:21:06Z)
• 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)
• 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)
• On Function Approximation in Reinforcement Learning: Optimism in the Face of Large State Spaces [208.67848059021915]
  We study the exploration-exploitation tradeoff at the core of reinforcement learning. In particular, we prove that the complexity of the function class $mathcalF$ characterizes the complexity of the function. Our regret bounds are independent of the number of episodes.
  arXiv  Detail & Related papers  (2020-11-09T18:32:22Z)
• 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)
• Robustly Learning any Clusterable Mixture of Gaussians [55.41573600814391]
  We study the efficient learnability of high-dimensional Gaussian mixtures in the adversarial-robust setting. We provide an algorithm that learns the components of an $epsilon$-corrupted $k$-mixture within information theoretically near-optimal error proofs of $tildeO(epsilon)$. Our main technical contribution is a new robust identifiability proof clusters from a Gaussian mixture, which can be captured by the constant-degree Sum of Squares proof system.
  arXiv  Detail & Related papers  (2020-05-13T16:44:12Z)

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.