# Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 21 of its 28 references that are in the map.
- First posted on arXiv 9 Apr 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Overcoming catastrophic forgetting in neural networks](https://mlsanity.com/paper/1612.00796/) (2016)
- [LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Models](https://mlsanity.com/paper/2403.13372/) (2024)
- [An Empirical Study of Catastrophic Forgetting in Large Language Models During Continual Fine-tuning](https://mlsanity.com/paper/2308.08747/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Model Merging in LLMs, MLLMs, and Beyond: Methods, Theories, Applications and Opportunities](https://mlsanity.com/paper/2408.07666/) (2024)
- [Continual Learning of Large Language Models: A Comprehensive Survey](https://mlsanity.com/paper/2404.16789/) (2024)
- [AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning dataset](https://mlsanity.com/paper/2504.16891/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Understanding Catastrophic Forgetting in Language Models via Implicit Inference](https://mlsanity.com/paper/2309.10105/) (2023)
- [Mitigating Catastrophic Forgetting in Large Language Models with Self-Synthesized Rehearsal](https://mlsanity.com/paper/2403.01244/) (2024)
- [Revisiting Catastrophic Forgetting in Large Language Model Tuning](https://mlsanity.com/paper/2406.04836/) (2024)
- [TRACE: A Comprehensive Benchmark for Continual Learning in Large Language Models](https://mlsanity.com/paper/2310.06762/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Spurious Forgetting in Continual Learning of Language Models](https://mlsanity.com/paper/2501.13453/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Scaling Laws for Forgetting When Fine-Tuning Large Language Models](https://mlsanity.com/paper/2401.05605/) (2024)
- [Mitigating Catastrophic Forgetting in Language Transfer via Model Merging](https://mlsanity.com/paper/2407.08699/) (2024)
- [Scaling Laws for Forgetting during Finetuning with Pretraining Data Injection](https://mlsanity.com/paper/2502.06042/) (2025)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)

## Abstract (arXiv)

Heavy supervised fine-tuning on a target domain can strongly suppress capabilities that were present in the base model. We study this phenomenon in formal mathematics using Goedel-Prover-V2, an open-source model heavily trained on 1.8 million formal-math examples. After domain specialization, the model almost completely loses its ability to produce valid tool calls, even when explicitly instructed to use tools, dropping from 89.4% function-calling accuracy in the base model to nearly 0%. We ask whether this agentic collapse is permanent or instead reversible. To answer this question, we fine-tune the specialized model on a small amount of Lean-specific tool-use data. Remarkably, as few as 100 agentic traces are sufficient to restore strong tool-calling behavior. Importantly, this recovery is not the result of reward hacking or benchmark-specific optimization: the recovery data is entirely drawn from the Lean setting, where the model uses natural-language queries to search the Mathlib library for relevant theorems and lemmas, yet the regained capability transfers well beyond that domain. In particular, these same 100 Lean-specific traces improve performance on the Berkeley Function Calling Leaderboard from near zero to 83.8%, approaching the base model's 89.4% despite the mismatch in task distribution and protocol. The recovered capability is also practically useful in-domain. On ProofNet, pass@32 improves from 21.51% to 25.81%. Together, these results show that heavy domain supervised fine-tuning can suppress general tool-use ability without permanently erasing it, and that a small amount of domain-specific agentic data can awaken dormant tool-use capabilities.