literature_search is incorrectly gated by planner model instead of worker model

[idrassi]

Summary

literature_search availability is currently decided from the planner model, but the search is actually executed by the worker backend.

This creates a mismatch for mixed-backend runs such as:

openprover --theorem examples/cauchy_schwarz.md \
  --planner-model opus \
  --worker-model minimax-m2.5 \
  --no-isolation

In that setup, the planner is allowed to choose literature_search, but the worker backend (minimax-m2.5 via local/vLLM) does not support web search.

Current behavior

The planner sees literature_search as available when --no-isolation is enabled and the planner model is not local.

However, _handle_literature_search() executes the search through self.worker_llm.call(..., web_search=True), so the worker backend needs to support
web search.

For local/vLLM workers, web_search=True is ignored, which means the run silently degrades: the UI and planner think search is available, but the
worker call has no real web access.

Expected behavior

literature_search should be gated by the worker backend's actual web-search capability, not by the planner model.

At minimum:

• --no-isolation should fail fast when the worker model cannot perform web search
• the runtime should not silently allow literature_search with a non-search-capable worker
• older runs or edge cases should degrade safely instead of pretending search is available

Why this matters

This is a correctness issue in mixed planner/worker configurations and can mislead the planner into believing it has access to literature search
when it does not.