MOTO v1.0.9

# MOTO v1.0.9

## Features

  - Users can now utilize ChatGPT subscription through oAuth for inference, in replacement of or in combination with OpenRouter/LM studio.
  - Users can now do proof-only solving by disabling paper writing under the acceptable outputs control, this enables the existing brainstorming + Lean 4 automated proof solving loop without automated research paper writing.

## Changes

  - Updated proof verification prompts to prioritize direct user-prompt solution attempts and carry brainstorm topic/source-title context through theorem discovery, lemma search, SMT translation, and Lean formalization.
  - Persisted advanced runtime settings for proof concurrency, Lean/SMT options, and OpenRouter free-model fallback controls.
  - Lean 4 proof writing mode has stronger emphasis on seeking novelty.
  - Cleaned up .cursor rules and aligned them with program where outdated.
  - Removed old/outdated code and scaffolding.
  - Improved live activity GUI logging.
  - Fresh starts now open on the main Autonomous screen instead of restoring the last viewed screen.
  - Cleaned up main directory.
  - Topic selection brainstorming sessions now emphasize to aggressively pick topics that solve the user's whole prompt at once where possible.
  - Expanded GUI live activity logging before truncation.

## Bug Fixes

  - Proof-solving attempts now receive the complete source paper or brainstorm context, making all models much more effective at solving Lean proof targets. Prior to this fix, all proof attempts were missing the accompanying brainstorm/paper which meant there was no Top-P exploratin architecture assisting proof solving. This is why only SOTA models were able to solve proofs before.
  - Hardened diagnostic logging against CodeQL log-injection findings and cleaned up first-party CodeQL warning-level frontend/backend issues.
  - Performed CodeQL audit and made minor fixes.
  - Added dedupe script for duplicate proof context, greatly reducing duplicate proof context.
  - Removed hidden context/max-token fallbacks and fixed compiler RAG budgeting so LM Studio, OpenRouter, and Codex use user-configured limits.
  - Fixed compiler High Parameter rigor proofs so Lean-verified proofs are ranked and indexed under the active paper.

  Authored by Patrick White, Patrick@Intrafere.com

Author: Pat

.cursor/rules/api-key-controls.mdc

@@ -0,0 +1,17 @@
+---
+description: Developer mode gating for hidden frontend controls
+alwaysApply: false
+---
+
+# Developer Mode Gates
+
+Developer mode is a hidden frontend switch toggled by pressing `Shift + Z + X`. The state is stored in localStorage as `developerModeSettingsEnabled` and should stay centralized through `developerModeEnabled` props or the same storage key.
+
+Known gated surfaces:
+- `LeanOJ Proof Solver` appears in the mode selector only while developer mode is enabled. If developer mode is turned off while `appMode === 'leanoj'`, the app should return to autonomous mode.
+- Supercharge checkboxes in Aggregator, Compiler, Autonomous, LeanOJ, and related role settings are developer-only. Start/request payloads must force `supercharge_enabled` false unless developer mode is currently enabled.
+- Creativity Emphasis Boost checkboxes beside Aggregator, Autonomous, and LeanOJ start controls are developer-only for now. Start/request payloads must force `creativity_emphasis_boost_enabled=false` unless developer mode is currently enabled; keep this gate isolated so the feature can later move to standard mode cleanly.
+- Raw JSON settings editors and developer-only model/settings toggles are developer-only and should close or hide when developer mode is disabled.
+- Boost copy may mention Supercharge only when developer mode is enabled.
+
+When adding a new hidden or experimental frontend control, gate both the visible UI and any request/runtime payload field behind developer mode. Do not rely on hiding the checkbox alone.

.cursor/rules/developer-mode-gates.mdc

@@ -1,4 +1,5 @@
 ---
+description: LaTeX renderer security, KaTeX parsing, and large-document rendering requirements
 alwaysApply: false
 ---
 
@@ -76,16 +77,15 @@ Dual rendering: **Rendered LaTeX View** (KaTeX math, dark theme on screen, white
 
 ## Rendering Pipeline (CRITICAL ORDER)
 
-Must execute in this exact order in `renderLatexToHtml()`:
+The raw conversion inside `renderLatexToHtml()` may include targeted preprocessing repairs between these anchors. Preserve these order constraints rather than treating every intermediate fix as a rule-level invariant:
 
 1. **`decodeHtmlEntities()`** — FIRST
-2. **`autoWrapMath()`** — Auto-wrap unwrapped math
-3. **`processTheoremEnvironments()`** — TikZ handling happens HERE (all three patterns: `\[...\]`, `$$...$$`, standalone)
-4. **`replaceSectionCommand()`** — Section headers
-5. **Text formatting, citations, footnotes, lists, tables, QED symbols**
-6. **KaTeX rendering** via `renderKatexSafely()` — `maxExpand: 5000`, skips HTML placeholder content
-7. **Line breaks/horizontal rules** (`\\` → `<br/>`, `\hrule` → `<hr/>`) — AFTER KaTeX
-8. **DOMPurify sanitization** — LAST
+2. Apply renderer-specific text/LaTeX repairs and auto-wrap unwrapped math before theorem/section/text formatting
+3. **`processTheoremEnvironments()`** — TikZ handling happens before KaTeX (all three patterns: `\[...\]`, `$$...$$`, standalone)
+4. **KaTeX rendering** via `renderKatexSafely()` — `maxExpand: 5000`, skips HTML placeholder content
+5. **Line breaks/horizontal rules** (`\\` → `<br/>`, `\hrule` → `<hr/>`) — AFTER KaTeX
+
+DOMPurify sanitization is intentionally outside `renderLatexToHtml()` and must run immediately after it at every HTML sink (`renderedHtmlSmall`, `RenderedChunk.renderedHtml`, and PDF helper rendering).
 
 **Critical:** `\\` line break conversion MUST be after KaTeX (valid syntax in `aligned`, `matrix`, etc.)
 
@@ -99,7 +99,7 @@ Must execute in this exact order in `renderLatexToHtml()`:
 
 **Auto-threshold**: Documents >50K chars (`LARGE_DOC_THRESHOLD`) auto-default to raw mode with a banner offering to switch to rendered view.
 
-**Invariant**: Each chunk independently runs the full `renderLatexToHtml()` → `DOMPurify.sanitize()` pipeline. The pipeline order within each chunk is identical to the single-document path.
+**Invariant**: Each chunk independently runs `renderLatexToHtml()` and then `DOMPurify.sanitize()`. Chunked and single-document paths must share the same conversion helpers and ordering anchors.
 
 ---
 
@@ -111,7 +111,7 @@ Must execute in this exact order in `renderLatexToHtml()`:
 
 **`sanitizeFilename()`**: Remove special chars, underscores for whitespace, truncate to 100 chars.
 
-**Backend PDF route**: `POST /api/download/pdf` — accepts `{html_body, title, word_count, date, models, outline, filename}`. Builds a standalone HTML document (KaTeX + LatexRenderer CSS both inlined from local filesystem + PDF print overrides that convert dark theme to light). `wait_until="load"` (no external requests). Runs `sync_playwright()` in `asyncio.get_running_loop().run_in_executor`. Returns `Response(content=pdf_bytes, media_type="application/pdf")`.
+**Backend PDF route**: `POST /api/download/pdf` — default/desktop mode accepts `{html_body, title, word_count, date, models, outline, filename}`. Builds a standalone HTML document (KaTeX + LatexRenderer CSS both inlined from local filesystem + PDF print overrides that convert dark theme to light). `wait_until="load"` (no external requests). Runs `sync_playwright()` in `asyncio.get_running_loop().run_in_executor`. Returns `Response(content=pdf_bytes, media_type="application/pdf")`. Generic mode returns `501`; current clients surface that backend unavailability and raw export remains available.
 
 **Playwright install**: `python -m playwright install chromium` — runs automatically in both launcher scripts after `pip install -r requirements.txt`. One-time ~150MB download of bundled Chromium (no system Chrome/Chromium required). Failure is non-fatal (warning shown, startup continues).
 
@@ -179,7 +179,7 @@ When a frontend storage prefix is active for multi-instance shared-origin use, t
 5. TikZ environments MUST be pre-processed — KaTeX cannot render them; remove surrounding math delimiters (all three patterns)
 6. KaTeX maxExpand MUST be 5000
 7. Line break conversion MUST happen AFTER KaTeX — prevents SVG corruption
-8. Rendering pipeline order MUST be preserved (same order in each chunk)
+8. Rendering pipeline ordering anchors MUST be preserved (same helpers/order in each chunk)
 9. Raw text view never processes HTML — plain text only
 10. PDF generation captures sanitized content
 11. Chunks MUST split at safe boundaries (section headers, double-newlines) — never mid-math-environment

.cursor/rules/hosted-web-contract.mdc

@@ -1,4 +1,5 @@
 ---
+description: Core code-change, rule-update, workflow-mode, and proof-runtime invariants
 alwaysApply: true
 ---
 
@@ -16,21 +17,24 @@ alwaysApply: true
 
 6.) For config/preset files with repeated literal values, never patch by replacing a shared literal alone. Anchor edits to the exact object/block being changed and verify the diff only touches the intended target.
 
-7.) Any REST shape, auth contract, WebSocket event, or `/api/features` capability change that affects the web wrapper must update **code, the relevant rule(s), and `api_contract_version` in `/api/features`** in the same approved merge. The live backend's `GET /openapi.json` is the machine-readable REST schema contract.
+7.) Any REST shape, auth contract, `/api/features` capability, or web-consumed WebSocket contract change must update **code, the relevant rule(s), and `api_contract_version` in `/api/features`** in the same approved merge. The live backend's `GET /openapi.json` is the machine-readable REST schema contract.
 
 8.) Only ONE workflow mode may be active at a time (Aggregator, Compiler, Autonomous Research, or LeanOJ Proof Solver). This constraint applies identically in both default mode and generic mode. Start conflict checks must be serialized and include pending/background-task activity flags such as `autonomous_coordinator.is_active`, not only persisted `state.is_running` fields.
 
-9.) Lean 4 and SMT features are always gated on `lean4_enabled`, `lean4_lsp_enabled`, and `smt_enabled` runtime flags. All three default false, must stay silent and side-effect-free when disabled, and must never ship Lean or Z3 toolchains or Python wheels into `requirements-generic.txt`, `Dockerfile`, or `docker/entrypoint.sh` (hosted image stays Lean-free and Z3-free). Lean 4 is authoritative formal checking for every stored proof and is necessary for LeanOJ final solutions; SMT contributes hints only. Z3 executable paths are trusted startup/operator configuration only, must be rejected as runtime API input, and must resolve to a `z3`/`z3.exe` executable. Automated proof candidates must directly serve the user prompt, not merely be non-trivial or novel.
+8b.) Autonomous Research and Single Paper Writer expose run-level Allowed Outputs (`allow_mathematical_proofs`, `allow_research_papers`); at least one must be true. Both true preserves existing workflow behavior. The Mathematical Proofs checkbox is the user-facing Lean proof-output enable path and must either sync/enable the runtime proof setting or the backend must reject proof-only/proof-requested starts when Lean is unavailable. Disabling papers must not disable brainstorming itself; proof-only autonomous runs must not silently become brainstorm-only loops and must reset durable workflow state to the next topic/exploration boundary after proof work instead of leaving `pre_paper_compilation`. Disabling proofs must skip proof-output work without affecting developer-only creativity boost behavior.
+
+9.) Lean 4 and SMT features are gated by runtime flags: `lean4_enabled` gates Lean proof execution/model proof work, `lean4_lsp_enabled` only gates the optional persistent LSP optimization (subprocess Lean must still work when it is false), and `smt_enabled` gates Z3/SMT hint generation. All three default false; when disabled they must not invoke their corresponding toolchains, spend proof-model calls, or block workflows, and must never ship Lean or Z3 toolchains or Python wheels into `requirements-generic.txt`, `Dockerfile`, or `docker/entrypoint.sh` (hosted image stays Lean-free and Z3-free). Lean 4 is authoritative formal checking for every stored proof and is necessary for LeanOJ final solutions; SMT contributes hints only, and only valid `unsat` SMT checks become suggested Lean tactics. Z3 executable paths are trusted startup/operator configuration only, must be rejected as runtime API input, and must resolve to a `z3`/`z3.exe` executable. Automated proof candidates should directly serve the user prompt and be novelty-first before Lean cost, but once Lean accepts real proof code it must be preserved and novelty-ranked under the actual proved statement; statement mismatch downshifts storage instead of discarding. Do not spend proof attempts building a general known-knowledge base of routine helpers, standard Mathlib/textbook facts, or merely non-trivial background lemmas. LeanOJ final master-proof edits may use standard facts inline to solve the template, but must not accumulate a separate known-knowledge library.
 
 10.) LeanOJ initial topic generation and brainstorm submitters always run in parallel and feed one validator that batch-validates up to 3 topics/submissions. Initial topic candidates/selection must be broad locked foundation questions covering the whole LeanOJ solution route, not narrow sublemma/tactic/local-repair topics. Recursive brainstorming has no separate recursive-topic prepass and must not re-inject the initial selected topic as active steering context; it uses the shared accepted proof-memory database plus the current proof/failure context. Accepted brainstorm memory must preserve occurrence-specific chronological metadata even for duplicate idea text. Never implement active LeanOJ topic or brainstorm phases as round-robin/serial submitter calls; one hung submitter must not halt the phase.
+10b.) Developer-enabled LeanOJ Creativity Emphasis Boost applies to every fifth valid queued initial-topic and brainstorm submission per submitter. It only adds optional near-solution/adjacent-solution creativity pressure when apparent and potentially very helpful; validation remains unchanged, accepted/rejected WebSocket payloads mark `creativity_emphasized`, and the block is skipped for that slot if it would overflow the configured prompt budget.
 
-11.) LeanOJ stop/crash/restart is resumable by default. `Clear Progress` / `/api/leanoj/clear?confirm=true` is the only intentional reset path. Start/restart should choose the best matching/resumable persisted session by proof context, not blindly create a new session or pick the latest file.
+11.) LeanOJ stop/crash/restart preserves resumable state by default. `Clear Progress` / `/api/leanoj/clear?confirm=true` is the only intentional reset path. Start/restart should choose the best matching/resumable persisted session by proof context, not blindly create a new session or pick the latest file; automatic model-work restart on backend boot is opt-in via runtime config.
 
-12.) LeanOJ OpenRouter credit exhaustion or no-fallback provider configuration errors are non-retryable pauses, not proof-attempt failures. Do not let API credit/config failures inflate final proof attempt loops.
+12.) LeanOJ and autonomous proof-check recoverable provider-credit exhaustion should preserve workflow checkpoints and pause rather than become proof-attempt failures. Hard configuration/privacy/missing-key errors should fail visibly with a user-repair path instead of inflating proof attempt loops. `Retry OpenRouter` / `/api/openrouter/reset-exhaustion` wakes currently waiting in-process credit pauses after credits are restored; stopped/restarted runs resume through their persisted LeanOJ/proof checkpoint state.
 
-13.) LeanOJ/RALPH final-proof loop checkpoints may only be user-configurable feedback checkpoints, not hidden loop shutdowns. The durable `master_proof.lean` is the authoritative working draft, and every accepted master-proof edit must pass an in-memory Lean gate before persistence: `needs_more_time=true` runs Lean with `sorry`/`admit` placeholders allowed but still requires parse/typecheck, template preservation, and no fake proof devices; `needs_more_time=false` runs Lean placeholder-free and then final semantic review against the user prompt/template before the run stops as verified. Final-proof mode is edit-only: it must not be offered, shown, or taught `stuck_needs_brainstorm`, raw `need_more_brainstorming`, failed-attempt counts, or any path transition. It may see the most recent 5 final attempts as compact execution feedback (Lean errors, stale edit rejections, JSON truncation, watchdog/no-progress notices) so it can avoid repeating failed edits. Lean/template rejection, semantic-review rejection, conservative no-progress/stale-edit watchdog feedback, and validator rejection of non-progressive shortening edits must preserve the master proof and persist structured continuation feedback; non-user-forced no-progress handoffs should gather recursive brainstorm context before re-entering final mode.
+13.) LeanOJ/RALPH final-proof loop checkpoints may be user-configurable feedback checkpoints or conservative no-progress/stale-edit watchdog handoffs; they must not mark success or discard the durable draft. LeanOJ start requests expose configurable phase caps (`max_initial_brainstorm_accepts`, `max_recursive_brainstorm_accepts`, `final_attempts_per_cycle`); `final_attempts_per_cycle` bounds failed final verification/edit attempts before the next path decision/handoff, so accepted `needs_more_time=true` edits can extend a cycle while they keep passing the intermediate Lean gate. The durable `master_proof.lean` is the authoritative working draft, and every accepted master-proof edit must pass an in-memory Lean gate before persistence: `needs_more_time=true` runs Lean with `sorry`/`admit` placeholders allowed but still requires parse/typecheck, template preservation, and no fake proof devices; `needs_more_time=false` runs Lean placeholder-free and then final semantic review against the user prompt/template before the run stops as verified. Final-proof mode is edit-only: it must not be offered, shown, or taught `stuck_needs_brainstorm`, raw `need_more_brainstorming`, failed-attempt counts, or any path transition. It may see the most recent 5 final attempts as compact execution feedback (Lean errors, stale edit rejections, JSON truncation, watchdog/no-progress notices) so it can avoid repeating failed edits. Lean/template rejection, semantic-review rejection, conservative no-progress/stale-edit watchdog feedback, and validator rejection of non-progressive shortening edits must preserve the master proof and persist structured continuation feedback; non-user-forced no-progress handoffs should gather recursive brainstorm context before re-entering final mode.
 
-14.) LeanOJ/RALPH final verification must remain placeholder-free, but Lean-accepted scaffolds containing `sorry`/`admit` should be saved as partial proofs for future context. Partial proofs are citeable incomplete references only; never count them as verified solutions and never accept fake `axiom`/`constant`/`opaque` proof devices.
+14.) LeanOJ/RALPH final verification must remain placeholder-free, but Lean-accepted scaffolds containing `sorry`/`admit` and Lean-accepted non-final-ready code should be saved as partial/supporting proofs for future context. Partial/scaffold checks may use subprocess fallback even when LSP mode is enabled. Partial proofs are citeable incomplete references only; never count them as final verified solutions and never accept fake `axiom`/`constant`/`opaque` proof devices. LeanOJ proof-gated brainstorm `lean_proof` submissions are preserved once Lean and integrity checks pass; brainstorm validation can classify usefulness/context role but should not veto the verified artifact.
 
 15.) Parent/user-selected phases have hierarchy precedence over child branches. When a parent phase starts (LeanOJ forced final loop, autonomous paper writing, Tier 3 final answer/final selection), lower-tier brainstorm/topic/path child tasks must stop or be ignored. LeanOJ `Skip Brainstorm` locks the run into the final loop until the configured final-attempt cycle is exhausted; model/path requests for more brainstorming cannot override that user action early. `Force Brainstorm` is a separate explicit user override that returns to recursive brainstorming while preserving proof progress.