In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator

• URL: http://arxiv.org/abs/2507.17780v1
• Date: Wed, 23 Jul 2025 00:49:32 GMT
• Title: In Reverie Together: Ten Years of Mathematical Discovery with a Machine Collaborator
• Authors: Randy Davila, Boris Brimkov, Ryan Pepper,
• Abstract summary: We present four open conjectures in graph theory generated by the automated conjecturing system textttTxGraffiti.<n>Each conjecture is concise, grounded in natural graph invariants, and empirically validated across hundreds of graphs.<n>We aim to inspire both human mathematicians and AI systems to engage with them--not only to solve them, but to reflect on what it means when machines participate meaningfully in the creative process of mathematical thought.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present four open conjectures in graph theory generated by the automated conjecturing system \texttt{TxGraffiti}. Each conjecture is concise, grounded in natural graph invariants, and empirically validated across hundreds of graphs. Despite extensive effort, these statements remain unresolved--defying both proof and counterexample. They are not only mathematical challenges but creative expressions--born of symbolic pattern recognition and mathematician-defined heuristics, refined through years of human dialogue, and now offered back to the community as collaborative artifacts. These conjectures invite not only formal proof, but also reflection on how machines can evoke wonder, spark curiosity, and contribute to the raw material of discovery. By highlighting these problems, we aim to inspire both human mathematicians and AI systems to engage with them--not only to solve them, but to reflect on what it means when machines participate meaningfully in the creative process of mathematical thought.

Related papers

• From Euler to AI: Unifying Formulas for Mathematical Constants [0.0]
  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.
  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)
• Automated conjecturing in mathematics with \emph{TxGraffiti} [0.0]
  emphTxGraffiti is a data-driven computer program developed to automate the process of generating conjectures. We present the design and core principles of emphTxGraffiti, including its roots in the original emphGraffiti program.
  arXiv  Detail & Related papers  (2024-09-28T15:06:31Z)
• Artifical intelligence and inherent mathematical difficulty [0.0]
  We first present an updated version of a traditional argument that limitative results from computability and complexity theory show that proof discovery is an inherently difficult problem. We then illustrate how several recent applications of artificial intelligence-inspired methods do indeed raise novel questions about the nature of mathematical proof.
  arXiv  Detail & Related papers  (2024-08-01T20:08:31Z)
• Artificial intelligence and machine learning generated conjectures with TxGraffiti [0.0]
  We outline the machine learning and techniques implemented by TxGraffiti. We also announce a new online version of the program available for anyone curious to explore conjectures in graph theory.
  arXiv  Detail & Related papers  (2024-07-03T01:03:09Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  Minimo is an agent that learns to pose problems for itself (conjecturing) and solve them (theorem proving) We combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains.
  arXiv  Detail & Related papers  (2024-06-30T13:34:54Z)
• Apriori Knowledge in an Era of Computational Opacity: The Role of AI in Mathematical Discovery [0.7673339435080445]
  We argue that the opacity of modern LLMs and DNNs creates obstacles in obtaining apriori mathematical knowledge from them.<n>We claim though that if a proof-checker automating human forms of proof-checking is attached to such machines, then we can obtain apriori mathematical knowledge from them.
  arXiv  Detail & Related papers  (2024-03-15T21:38:26Z)
• 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)
• AI for Mathematics: A Cognitive Science Perspective [86.02346372284292]
  Mathematics is one of the most powerful conceptual systems developed and used by the human species. Rapid progress in AI, particularly propelled by advances in large language models (LLMs), has sparked renewed, widespread interest in building such systems.
  arXiv  Detail & Related papers  (2023-10-19T02:00:31Z)
• Learning Algebraic Representation for Systematic Generalization in Abstract Reasoning [109.21780441933164]
  We propose a hybrid approach to improve systematic generalization in reasoning. We showcase a prototype with algebraic representation for the abstract spatial-temporal task of Raven's Progressive Matrices (RPM) We show that the algebraic representation learned can be decoded by isomorphism to generate an answer.
  arXiv  Detail & Related papers  (2021-11-25T09:56:30Z)
• 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)
• Machine Number Sense: A Dataset of Visual Arithmetic Problems for Abstract and Relational Reasoning [95.18337034090648]
  We propose a dataset, Machine Number Sense (MNS), consisting of visual arithmetic problems automatically generated using a grammar model--And-Or Graph (AOG) These visual arithmetic problems are in the form of geometric figures. We benchmark the MNS dataset using four predominant neural network models as baselines in this visual reasoning task.
  arXiv  Detail & Related papers  (2020-04-25T17:14:58Z)

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.