COMPOSE: Composing Future Theorems from Citations and Formal Structure

A generated plausible future mathematical claim must satisfy two constraints: it should follow the direction of prior work and respect the formal dependencies that constrain the validly of the claim. 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, the task of generating a plausible future theorem-like claim for an anchor paper, using two complementary sources of context: its scientific citation graph ,and its aligned formal theorem dependency graph. To address this setting, we propose COMPOSE, a dual-graph framework that combines scientific citation context with formal mathematical structure to condition a language model. To support this setting, we construct a dataset of 108K paired scientific-formal graphs 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.