Problem
The recursive prover's parent proof step (_prove_parent_with_children) calls the LLM with use_extended_thinking=self._prover_config.use_extended_thinking, but the test harness and default pipeline configuration run with extended_thinking=False.
For competition-level problems (Putnam, IMO), proving the parent theorem from child lemma axioms often requires multi-step reasoning:
- Set equality proofs (
{n | P(n)} = {1}): need ext → biconditional → forward witness + backward impossibility argument
- Modular arithmetic: need case analysis on residues, which requires planning before tactic selection
- Induction/descent: need to identify the right induction variable and base case
Without extended thinking, the model gets ~900 output tokens to produce both the proof strategy and Lean 4 tactics. That's insufficient for Putnam-level proofs.
Evidence
From the Putnam 2024 A1 E2E run (PR #104):
llm_request extended_thinking=False max_tokens=4096
llm_response output_tokens=880 → recursive_prover_parent_failed failure_type=stuck_goal retry=1
llm_response output_tokens=986 → recursive_prover_parent_failed failure_type=stuck_goal retry=2
llm_response output_tokens=923 → recursive_prover_parent_failed failure_type=stuck_goal retry=3
The model uses 880-986 tokens per attempt but can't close the proof. Extended thinking would give it a dedicated reasoning budget before generating tactics.
Proposed Fix
Two options (not mutually exclusive):
Option A — Adaptive extended thinking based on proof complexity:
If the parent theorem involves set equality, quantifier alternation, or >3 child lemmas, automatically enable extended thinking for the parent proof step:
use_thinking = self._prover_config.use_extended_thinking
if not use_thinking and self._should_use_extended_thinking(node, children):
use_thinking = TrueWhere _should_use_extended_thinking checks heuristics like:
- Statement contains
= { (set equality)
- Statement has nested
∀ ... ∃ (quantifier alternation)
- Node has >3 children (complex assembly)
- Retry count >1 (previous attempts failed without thinking)
Option B — Always enable extended thinking for parent proofs:
Parent proofs are the hardest step (assembling child results into the main theorem). The cost of extended thinking (~2x tokens) is small relative to the cost of 3 failed retries + diagnosis + reformulation.
Impact
- Putnam 2024 A1 currently fails at parent assembly despite correct decomposition into 5 valid child lemmas
- "Beyond the Library" (arXiv:2606.31134) achieves 91.3% on PutnamBench — they use extended reasoning at the assembly step
- This is likely the single highest-impact change for competition-level proof success rate
References
Problem
The recursive prover's parent proof step (
_prove_parent_with_children) calls the LLM withuse_extended_thinking=self._prover_config.use_extended_thinking, but the test harness and default pipeline configuration run withextended_thinking=False.For competition-level problems (Putnam, IMO), proving the parent theorem from child lemma axioms often requires multi-step reasoning:
{n | P(n)} = {1}): needext→ biconditional → forward witness + backward impossibility argumentWithout extended thinking, the model gets ~900 output tokens to produce both the proof strategy and Lean 4 tactics. That's insufficient for Putnam-level proofs.
Evidence
From the Putnam 2024 A1 E2E run (PR #104):
The model uses 880-986 tokens per attempt but can't close the proof. Extended thinking would give it a dedicated reasoning budget before generating tactics.
Proposed Fix
Two options (not mutually exclusive):
Option A — Adaptive extended thinking based on proof complexity:
If the parent theorem involves set equality, quantifier alternation, or >3 child lemmas, automatically enable extended thinking for the parent proof step:
Where
_should_use_extended_thinkingchecks heuristics like:= {(set equality)∀ ... ∃(quantifier alternation)Option B — Always enable extended thinking for parent proofs:
Parent proofs are the hardest step (assembling child results into the main theorem). The cost of extended thinking (~2x tokens) is small relative to the cost of 3 failed retries + diagnosis + reformulation.
Impact
References