Add real demo outputs from recorded runs

[crqu]

Problem

The documentation suite is thorough (QUICKSTART.md, TUTORIAL.md, FAQ.md, etc.), but all examples are illustrative/mock — no real captured output from actual runs exists in the repo. A mathematician evaluating ProofPartner has no way to see what a successful run actually produces before committing their API key and money.

Why this matters

This is the lowest-effort, highest-impact adoption improvement. People don't try tools they can't preview. A curated set of real outputs answers: "What will I get?" and "Is this worth $5 per run?"

Proposal

Record and commit 2–3 actual end-to-end runs with real output artifacts:

1. Simple olympiad problem — e.g., a miniF2F problem via explore → formalize → prove. Show the full terminal output, final .lean file, and cost breakdown. This is the "hello world" that proves the tool works.

2. Exploration flow — explore on a rough mathematical idea, showing the ranked conjecture table with confidence scores and difficulty ratings. Demonstrates the Stage 0 → Stage 1 value proposition.

3. Novel conjecture formalization — a conjecture not in any benchmark, showing type-first formalization, IntentJudge verification, and (ideally) a successful proof. This is the use case no competitor supports.

For each, commit:

• Terminal output (captured via script or tee)
• Generated .lean artifacts
• Cost summary
• Brief annotation explaining what happened at each stage

These could live in examples/ or docs/demos/.