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
• 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

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
  We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents.<n>We provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis.
  arXiv  Detail & Related papers  (2026-07-08T17:46:36Z)
• AI co-mathematician: Accelerating mathematicians with agentic AI [37.60588462488029]
  We introduce the AI co-mathematician, a workbench for mathematicians to interactively leverage AI agents to pursue open-ended research.<n>The AI co-mathematician is to provide holistic support for the exploratory and iterative reality of mathematical ideation, including literature search, computational exploration, theorem proving and theory building.<n>In early tests, the AI co-mathematician helped researchers solve open problems, identify new research directions, and uncover literature references.
  arXiv  Detail & Related papers  (2026-05-07T17:56:32Z)
• Math Takes Two: A test for emergent mathematical reasoning in communication [1.2891210250935148]
  Math Takes Two is a new benchmark designed to assess the emergence of mathematical reasoning through communication.<n>Motivated by the hypothesis that mathematical cognition in humans co-evolved with the need for precise communication, our benchmark tests whether two agents, without prior mathematical knowledge, can develop a shared symbolic protocol.
  arXiv  Detail & Related papers  (2026-03-30T08:28:48Z)
• Discovering mathematical concepts through a multi-agent system [3.820195410658766]
  We present a new multi-agent model for computational mathematical discovery.<n>Our system, conceived with research in mind, poses its own conjectures and then attempts to prove them.<n>We claim that the optimisation of the right combination of local processes can lead to surprisingly well-aligned notions of mathematical interestingness.
  arXiv  Detail & Related papers  (2026-03-04T19:13:36Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  We introduce Aletheia, a math research agent that iteratively generates, verifies, and revises solutions end-to-end in natural language.<n>Specifically, Aletheia is powered by an advanced version of Gemini Deep Think for challenging reasoning problems.<n>We demonstrate Aletheia from Olympiad problems to PhD-level exercises and most notably, through several distinct milestones in AI-assisted mathematics research.
  arXiv  Detail & Related papers  (2026-02-10T18:50:15Z)
• Accelerating Scientific Research with Gemini: Case Studies and Common Techniques [105.15622072347811]
  Large language models (LLMs) have opened new avenues for accelerating scientific research.<n>We present a collection of case studies demonstrating how researchers have successfully collaborated with advanced AI models.
  arXiv  Detail & Related papers  (2026-02-03T18:56:17Z)
• 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.