Make agent loop action-based: planner chooses what to do next

Fix 6 information flow breaks in the agent loop

Add creativity agent for lateral thinking about proof strategies

Add trashcan icon to session list for quick delete (no confirmation)

Fix delete confirmation message — global lessons are preserved

Add delete session button to dashboard GUI

Add diagnostic analysis — agent reasons about WHY proofs fail

Don't auto-add imports from retrieval modules — some aren't built

Add by-block collapse to fix the most common indentation bug

Add exact? feedback loop and full lemma signatures

Tell lean agent to use exact fully-qualified lemma names and add imports

Stop auto-extractor from promoting raw error strings as global lessons

Guide planner web search toward Lean 4 / Mathlib4 only

Stop web search from polluting lessons and code synthesis

Fix the core indentation bug via prompting: single-line have, explicit examples