On Compositional Learning Behaviours in Formal Mathematics

Language model-based AI agents capable of conquering the Olympiad-level tail of formal mathematics require Compositional Learning Behaviours (CLBs): the capacity to ground and recombine novel symbolic structures in context, beyond mere recombination of prelearned atoms. We propose **S2B-LM**, an adaptation of the CLB-evaluating Symbolic Behaviour Benchmark that removes numerical processing as a confound and adds chain-of-thought scaffolding to elicit rather than merely probe latent CLB competency. Cross-evaluating ten Lean 4 theorem provers on CLB competency in S2B-LM and miniF2F whole-proof performance, we find correlational and causal evidence of our claim: First, a necessary-condition analysis via quadrant test yields $p=0.004$, with model scale being ruled out as a confound. Second, extracting a CLB-encoding activation direction from *DeepSeek-Prover-V2-7B* using S2B-LM traces via Contrastive Activation Addition and applying it during miniF2F whole-proof generation on the AIME subset, CLB suppression collapses solve rate from $32.3$% to $2.9$%, without loss of coherence, while suppressing a random activation direction of equal magnitude leaves it at $31.9$%. Together, these results show that CLB competency is **necessary but not sufficient** for the hard tail of formal mathematical verification.