01
+Start with a proof already in the reading room.
++ Choose a sample proof, switch between the paper and Lean views, and + inspect its proof map and verification evidence. Recorded examples show + the complete explanation interface without making a model request. +
+-
+
- Select a sentence, equation, or Lean declaration. +
- Choose an action such as More details or Connect to Lean. +
- Follow source chips back to the exact paper or Lean location. +
- Check the verification disclosure before treating a formal claim as checked. +
02
+Use a paper of your own.
+
+ The upload workspace requires a PDF and accepts optional individual
+ .lean files or a ZIP of Lean sources. Files are parsed in
+ your browser and are not added to the public proof library.
+
+ Only the selected passage and bounded nearby context are sent when you + explicitly request an explanation. Uploaded Lean is labeled unverified. +
+03
+Enable live AI explanations.
+
+ Keep the OpenAI key on the server. Never paste it into browser code,
+ commit it to Git, or give it a NEXT_PUBLIC_ prefix.
+
Local development
+
+ {`cp .env.example .env.local
+# Edit .env.local and set:
+OPENAI_API_KEY=your_key_here
+OPENAI_MODEL=gpt-5.6
+npm run dev`}
+
+ + Restart the development server after changing environment variables. + Without a key, the reader remains available and explanation requests + return an explicit configuration error. +
+Hosted deployment
+
+ Add OPENAI_API_KEY using the host's secret manager. Add
+ OPENAI_MODEL, EXPLAIN_RATE_LIMIT_PER_HOUR, and
+ an explicit PUBLIC_PROOF_IDS allowlist as environment
+ variables, then deploy a new version.
+
04
+Know what each label promises.
+-
+
- Paper states +
- The claim appears in the supplied paper source. +
- Lean verifies +
- A recorded toolchain checked the named formal declaration. +
- Curated correspondence +
- A human-authored mapping connects paper and Lean locations. +
- AI explains +
- Generated interpretation grounded in the bounded supplied context. +
+ A successful Lean build does not by itself prove that the formal theorem + perfectly translates the paper. Interactive Proof keeps those claims + separate so readers can inspect both. +
+ + Read the evaluation and security methodology + +05
+Run and verify the project locally.
+
+ {`npm ci
+cp .env.example .env.local
+npm run dev
+
+# Before opening a pull request
+npm run proof:validate
+npm run eval:validate
+npm test
+npm run typecheck
+npm run lint
+npm run build`}
+
+ + Node.js 24 is required. Chromium is needed only for browser tests, and + Lean is needed only when regenerating verification evidence for a full + local proof package. +
+