Socratic Math Tutor — an agentic, ground-truth-verified tutor

An AI math tutor that guides students step by step instead of handing over answers, and grounds every correctness judgment in a real symbolic math engine (SymPy) rather than the LLM's own (error-prone) arithmetic.

Why it's an agent, not a chatbot

It runs a real tool-use loop: Claude decides to verify a step → calls the math engine → reads the result → responds Socratically. The model never asserts correctness on its own — the ground truth is the math engine.

student step ──▶ Claude (agent loop) ──▶ check_step() [SymPy]
                      ▲                         │ valid / invalid + where
                      └───── hint, not answer ──┘

Two ground-truth engines (neurosymbolic)

The agent routes each student step to the right verifier:

• SymPy (mathcheck.py) — decides computational algebra (simplify, expand, solve). Instant, exact, no hallucinated correctness.
• Lean 4 + Mathlib (lean_verify.py) — verifies deductive proofs (induction, divisibility, inequalities). The agent autoformalizes the student's claim into Lean; Lean's kernel certifies it.

SymPy handles computation, Lean handles proof — the same split DeepMind uses (AlphaGeometry's symbolic engine vs. AlphaProof's Lean). Lean is a local feature and degrades gracefully when absent — see lean/SETUP.md.

Two frontends

• Classic (index.html, served by FastAPI at :8000) — KaTeX chat, Mermaid solution maps, Lean proof-reveal panel.
• OpenUI generative UI (openui-frontend/, Next.js at :3000) — the model composes the interface per reply in OpenUI Lang (sponsor: OpenUI): clickable strategy Buttons, Steps, verdict Callouts, collapsed Lean-proof Accordions. It proxies to the same Python brain (/api/chat → /api/tutor).

# terminal 1 — the brain
python3 -m uvicorn app:app --port 8000
# terminal 2 — the OpenUI frontend
cd openui-frontend && npm install && npm run dev   # http://localhost:3000

Run locally

pip install -r requirements.txt
export ANTHROPIC_API_KEY=sk-ant-...
uvicorn app:app --reload
# open http://localhost:8000

Try: Solve 3(x + 2) = 21, then submit a wrong step like 3x + 2 = 21 (forgot to distribute). The engine catches the exact error and the tutor asks a guiding question instead of fixing it for you.

Deploy on Render

1. Push this folder to a GitHub repo.
2. Render dashboard → New → Blueprint → pick the repo (render.yaml is detected).
3. Add the env var ANTHROPIC_API_KEY in the service settings.
4. Deploy. (Free plan sleeps when idle — first request after a nap is slow.)

Sponsor integration map (Tool Use criterion)

Wired: Claude (AWS) + Render + ClickHouse + Composio = 4.

Sponsor	Role	Status
Claude (AWS)	the tutoring agent	✅ wired (tutor.py)
Render	hosting	✅ wired (render.yaml)
ClickHouse	every verified step → tutor_events table → mastery analytics	✅ wired (sponsors.log_event)
Composio	autonomous Gmail progress reports — the "act" surface	✅ wired (sponsors.send_progress_report, POST /api/report)
OpenUI	generative tutoring UI (hint ladders, graphs)	hook: replace index.html
Airbyte	ingest curricula / problem banks	hook: feeds ClickHouse
TrueFoundry	gateway to route + govern Claude calls	hook: wrap the client in tutor.py

Both integrations degrade gracefully — with no credentials set they fall back to console logging, so the app always runs. To activate:

• ClickHouse — set CLICKHOUSE_HOST/USER/PASSWORD/DATABASE; the tutor_events table is auto-created on the first event.
• Composio — set COMPOSIO_API_KEY and connect a Gmail account once (Composio dashboard or connected_accounts.link); reports then send via GMAIL_SEND_EMAIL.

Go deep on 4–5, not shallow on all of them — judges reward real integration.

3-minute demo script

1. Enter a problem; submit a step with a mistake → tutor flags the exact wrong step (engine-verified) and asks a guiding question.
2. Fix it → tutor confirms and moves you forward.
3. Show the autonomous side: the agent emails a parent a progress report (send_progress_report) and the mastery dashboard updates (ClickHouse).

Files

• mathcheck.py — SymPy ground-truth verification (the spine)
• tutor.py — the agent loop, tools, and Socratic system prompt
• app.py — FastAPI server + session state
• index.html — the tutoring UI
• sponsors.py — integration hooks (ClickHouse, Composio, …)
• render.yaml — Render Blueprint