Add code deduplication to break proof search repetition loops

[crqu]

Problem

The LLM repeatedly generates identical failing Lean 4 code across proof search iterations. This wastes 20-33% of REPL compilation attempts.

Evidence

From PutnamBench trajectory analysis:

• Problem putnam_2003_b6: hash 315efc3d2f37 submitted 16 times (33% repetition rate)
• Problem putnam_2000_a4: hash b36ffca1f393 submitted 5 times (15% repetition rate)
• The error feedback loop does not help the LLM escape these attractors

Proposed fix

In IterativeProver:

1. Track a set of code hashes submitted per problem
2. Before compiling, check if the code hash was already tried
3. If duplicate detected:
   • Skip compilation
   • Add explicit "Do NOT generate this code again: " to the prompt
   • Or increase temperature for the next attempt
   • Or skip to next strategy

Impact

MEDIUM — saves 20-33% of wasted REPL calls and may force the LLM into novel proof attempts.

Files

• agentic_research/agents/prover.py (IterativeProver)