# COMPOSE: Composing Future Theorems from Citations and Formal Structure

arXiv: https://arxiv.org/abs/2605.30333 · HTML: https://mlsanity.com/paper/2605.30333/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 31 of its 43 references that are in the map.
- First posted on arXiv 28 May 2026.

## Builds on (most cited first, 30 of 31)

- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Text Embeddings by Weakly-Supervised Contrastive Pre-training](https://mlsanity.com/paper/2212.03533/) (2022)
- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Can LLMs Generate Novel Research Ideas? A Large-Scale Human Study with 100+ NLP Researchers](https://mlsanity.com/paper/2409.04109/) (2024)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [ResearchAgent: Iterative Research Idea Generation over Scientific Literature with Large Language Models](https://mlsanity.com/paper/2404.07738/) (2024)
- [SciMON: Scientific Inspiration Machines Optimized for Novelty](https://mlsanity.com/paper/2305.14259/) (2023)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [Human-LLM Compound System for Scientific Ideation through Facet Recombination and Novelty Evaluation](https://mlsanity.com/paper/2409.14634/) (2024)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Improving Scientific Hypothesis Generation with Knowledge Grounded Large Language Models](https://mlsanity.com/paper/2411.02382/) (2024)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [Enhancing Scientific Papers Summarization with Citation Graph](https://mlsanity.com/paper/2104.03057/) (2021)
- [LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving](https://mlsanity.com/paper/2506.22005/) (2025)
- [Learning to Predict Future-Aligned Research Proposals with Language Models](https://mlsanity.com/paper/2603.27146/) (2026)
- [GIANTS: Generative Insight Anticipation from Scientific Literature](https://mlsanity.com/paper/2604.09793/) (2026)
- [GoAI: Enhancing AI Students' Learning Paths and Idea Generation via Graph of AI Ideas](https://mlsanity.com/paper/2503.08549/) (2025)
- [FutureGen: A RAG-based Approach to Generate the Future Work of Scientific Article](https://mlsanity.com/paper/2503.16561/) (2025)

## Built on by (most cited first, 3 of 3)

- [MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures](https://mlsanity.com/paper/2607.27709/) (2026)
- [Beyond Correctness: Toward Automated Novelty Verification with Lean 4](https://mlsanity.com/paper/2608.14669/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)

## Abstract (arXiv)

A plausible future mathematical claim must satisfy two constraints: it should follow the direction of prior work and respect the formal dependencies that constrain what can validly follow. Existing approaches typically model only one of these sources, producing claims that are either weakly grounded or insufficiently motivated. We introduce grounded future mathematical generation, where the goal is to generate a plausible future theorem-like claim for an anchor paper using two complementary sources of context: its scientific citation graph and aligned formal theorem dependency graph. To address this setting, we propose COMPOSE, a dual-graph framework that conditions a language model on both scientific citation context and formal theorem structure. To support this setting, we construct a dataset of 108K paired scientific-formal graph examples from arXiv and Mathlib, together with a benchmark of 47K future papers from 2024--2025. Experiments show that COMPOSE outperforms strong baselines on retrieval to real future papers and achieves the best overall performance under LLM-judge evaluation, producing more grounded and mathematically richer outputs. These results show that future mathematical generation benefits from combining scientific context with formal structure. Project page is available at https://david-busbib.github.io/COMPOSE-page/.