Pie, the dependently typed teaching language of The Little Typer, is pedagogically near-ideal: just enough to teach dependent types and proof, and no black boxes. Yet its original implementation imposes barriers of its own: a heavyweight local setup, no interactive feedback, a fixed set of built-in types, and proofs written as flat terms with no incremental workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes let incomplete programs type-check and report each goal’s type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.