Development record · educational AI application
Interactive Proof
A paper reader built around a simple constraint: help a learner understand one proof step without losing the source, the formal code, or the boundary between evidence and explanation.
Development record
A proof-reading companion built as a full-stack system
The public repository moves from a proof-package architecture and reader shell through upload handling, bounded explanation routes, rich mathematical rendering, release checks, and a public upload-first flow.
- Paper reading with a selectable text layer and contextual actions
- Optional Lean context kept visibly separate from uploaded source and verified fixtures
- Server-side, bounded explanations with source disclosures, retry, follow-up, and cancellation states
Context
Interactive Proof began with a specific learning failure: a reader can follow the broad argument in a mathematical paper and still stop at one compressed sentence, equation, or proof step. Leaving the paper for a generic search loses the source location. Opening a formal repository introduces another language. A bare verification badge does not explain what was checked.
The problem was local, not general
The product does not try to answer mathematics in the abstract. It keeps one selected passage in view, adds nearby context, and asks the model for an explanation at the scale of the reader's question. Optional Lean source can connect the idea to formal code without being silently treated as verified.
That narrow interaction shaped the application boundary: the paper remains the source, Lean remains a distinct formal layer, and model prose remains generated interpretation.
A build window needs hard boundaries
The browser parses temporary uploads and sends only a bounded selection and nearby context when the reader explicitly requests help. The server validates the request, constructs the context bundle, and calls the Responses API with the key kept server-side. The application, not the model, renders source chips, verification badges, and build status.
Project timeline
The visible main branch is a cleaned, rebased release history—not the original PR-by-PR graph. The fuller development record survives in 22 closed pull requests opened from 13–20 Jul 2026. These checkpoints pair that build sequence with the commits that explain what shipped in the public Interactive Proof repository.
-
Build the proof reader
The first implementation wave assembled streamed explanations, CI and browser smoke coverage, a second proof package, and the selectable PDF.js reader.
Result: the project became an integrated reader with a clear place for source, formal code, explanation, and validation.
-
Put evidence around the core interaction
Release verification, disclosure, evaluation and security notes, accessibility acceptance coverage, the Devpost/demo package, and the private Sites deployment were added around the reader.
Result: the project had an evidence boundary and a public handoff, not only a working interface.
-
Expand the learning surface
Launch gates, deep links, themes, guided learning controls, proof-package authoring, a navigable proof map, instructor-authored guidance, and honest demonstrations were added as separate feature slices.
Result: the reader grew into a teachable workflow without hiding which parts were authored, verified, or generated.
-
Make the public journey upload-first
Ephemeral paper and Lean uploads turned the reader into a temporary workspace. The product could begin with a visitor's own material instead of a fixed catalogue, while the cleared proof fixture stayed available for deterministic checks.
Result: source handling became part of the product boundary, not an afterthought around a demo fixture.
-
Prepare the release handoff
Repository-wide autoreview findings were fixed, public setup documentation was added, and release media and deployment handoff were prepared before the final public branch was cleaned up.
Result: the work moved from feature completion to a release that another person could inspect and run.
-
Rebase the build into a public release
Rich mathematical rendering, learner-facing explanations, hydration fixes, deployment verification, upload-first documentation, and legacy-browser PDF support were consolidated into the clean release history.
Current state: a public educational application whose repository, documentation, and demo describe the same interaction and the same limits.
System
Keep four kinds of evidence visible
- Paper source: the uploaded passage and nearby context the reader selected.
- Formal layer: optional Lean source, curated mappings, and recorded verification metadata.
- Generated layer: a streamed explanation shaped by the bounded context bundle.
- Application state: selection location, follow-up history, retry behavior, and temporary workspace state owned by the application.
These layers can be related without being collapsed. A successful Lean build does not prove that a paper-to-code correspondence is perfect, and model prose does not create a source citation or verification badge.
An upload-first context boundary
PDF and optional Lean files are parsed in the browser and kept in the temporary workspace. When a reader asks for help, the client sends a bounded selection and nearby context to the server. The server validates size and source limits, constructs the application-defined context, and streams a response through the OpenAI Responses API.
Without a server-side key, the workspace remains available and the explanation request returns an explicit configuration error. The failure is visible; it is not replaced with fabricated output.
Proof packages and verification
The repository keeps a cleared proof fixture for deterministic validation. Package manifests record source references, mappings, prerequisites, and verification metadata; full local verification records the toolchain, command result, axiom audit, and output digest. Uploaded Lean is always labeled unverified.
Reader Evidence
The implemented interaction
The public application is more than an explanation endpoint. Its evidence is in the handoffs that keep the reader oriented:
- PDF.js renders the paper with a selectable text layer.
- A contextual selection menu opens a focused explanation action without losing the passage.
- The explanation panel streams plain-language and rich mathematical output.
- A source disclosure shows which supplied material shaped the answer.
- Follow-up questions retain the original selection, while retry and cancellation states keep failure recoverable.
- Optional uploaded Lean is available as context and is visibly marked unverified.
Current state
A public reader with explicit limits
Interactive Proof is publicly available as an upload-first workspace. A reader can provide a paper, optionally add Lean, select a passage, request a bounded explanation, inspect the supplied sources, ask a follow-up, and clear the temporary workspace.
What the repository proves
The project demonstrates full-stack implementation, evidence-boundary design, browser interaction, release validation, and a public deployment path. It does not claim measured learning gains, broad mathematical correctness, or automatic paper-to-Lean translation. Those are separate questions requiring separate evidence.
The important result is narrower and more useful: a difficult proof-reading moment became a concrete interaction with visible boundaries around source, formal verification, and generated help.
Artifacts