docs: add proposed AI-assisted proof ingestion roadmap section

[AkiraTamai]

Summary

Docs-only. Adds a single new docs/ROADMAP.md section at the end, ## AI-assisted proof ingestion and translator surface extension (proposed), as the Lean-side receiving task for the mumei-agent "Task 2-D: AI-driven Lean proof generation for unknown atoms" (that agent-side plan is still being written; no ✅ marker here since nothing is implemented).

It records two sub-tasks — (a) widening expr_translator lowering to shrink partial_translation (with the mandatory §8/§10 spec updates and compute_bridge_lemma_hash() recomputation), and (b) generalising IngestedAtom.auto_tactic so an externally supplied proof body can be injected into render_theorem — plus the soundness guards that must stay unchanged: promotion still depends only on _translator_contract_current / _lean_result_contract_current and a real lake build, MUMEI_LEAN_SKIP_LIVE=1 / no-Lake paths skip AI generation, and contract-constant changes must land with LEAN_TRANSLATOR_VERSION / LEAN_BRIDGE_LEMMA_HASH and the mumei-agent constants in the same change set.

PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest -q passes except tests/test_proofcert.py::test_representative_certificate_validates_against_schema, which fails on this box from a broken local jsonschema install (AttributeError on Draft202012Validator), unrelated to this diff.

Link to Devin session: https://app.devin.ai/sessions/f96c2ca334024b6699566ec540d8e391
Open in Devin Desktop: https://app.devin.ai/desktop/session/f96c2ca334024b6699566ec540d8e391?variant=devin
Requested by: @AkiraTamai

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

Devin Review found 1 potential issue.