Autonomous planning and definition resolution

[FluffyAIcode]

Summary

• add evidence/gap planning, creative move candidates, strategy tournaments, and research contracts
• add theorem-card retrieval, stepwise Lean search, atomic definitions, and autonomous definition resolution
• include the directly coupled offline checkpoint migrations here so this planning slice is independently testable; runtime activation remains in PR3

Test plan

• PYTHONPATH=. ~/.venv-distwan/bin/python -m pytest -q tests/inference_engine/bench/test_atomic_definition.py tests/inference_engine/bench/test_creative_decomposition.py tests/inference_engine/bench/test_definition_resolution.py tests/inference_engine/bench/test_strategy_tournament_stepwise.py (53 passed)
• PYTHON=~/.venv-distwan/bin/python bash scripts/run_local_ci.sh (1094 passed, 1 skipped)
• real Lean stepwise executor exercised after lake build Mathlib

Made with Cursor

[cursor]

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.