# Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 13 references that are in the map.
- First posted on arXiv 30 Jul 2026.

## Builds on (most cited first, 6 of 6)

- [RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics](https://mlsanity.com/paper/2505.12575/) (2025)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory](https://mlsanity.com/paper/2607.06447/) (2026)
- [ProofCouncil: An LLM Agent for Solving Open Mathematical Problems](https://mlsanity.com/paper/2607.09474/) (2026)

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

- [Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science](https://mlsanity.com/paper/2609.15983/) (2026)
- [EULER: Exploring Underused Links with Evidence-Checked Return for Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2609.00032/) (2026)
- [Continual Graph Memory for Mathematical Research Agents](https://mlsanity.com/paper/2610.02945/) (2026)
- [Euler: Towards Human-Centered Multi-Agent Mathematical Discovery](https://mlsanity.com/paper/2610.19864/) (2026)

## Abstract (arXiv)

Large language models can contribute useful ideas to mathematical research, yet long-horizon proof attempts remain difficult to coordinate, evaluate, and reproduce. We present Albilich, an open-source agentic harness for autoresearch in mathematics that combines long-horizon reasoning, computer algebra systems (CAS), literature retrieval, and persistent SQLite-based context management. We evaluate Albilich on the RealMath benchmark (Zhang et al. 2025) and on open problems in group theory from the Kourovka Notebook (Khukhro and Mazurov 2026). It solved 10/10 problems on RealMath with CAS and 9/10 with no CAS. On the Kourovka problems, Albilich produced a counterexample to Problem 21.142 and a proof of a strengthening of Problem20.2. Anablation on Problem 17.91 demonstrates 32.0% token reduction when CAS is enabled. An ablation on Problem 21.142 demonstrates higher verifier-rejection rate and failure to synthesize proof routes in the absence of the advisor agent. These results support Albilich as a human-steerable, CAS-boosted environment for scalable AI-assisted mathematical research.