# MOTO v1.1.01

## Features

  - Local memory is now enabled, prior sessions can now aid discoveries of new runs! Local proof-history access as verified proof corpora for a parallel Assistant role that retrieves up to 7 proof supports without blocking the main solver.
  - Added SyntheticLib feaures and coming-soon information on SyntheticLib™, "The Inventor's Dictionary". A shared novel discovery database that users contribute novel proofs to for access. This will operate as an optional extension to the local memory system, SyntheticLib is a global/shared memory system.
  - Added the Assistant role as a non-validating rolling proof-support layer that sees the user prompt, live solver feedback, and its current pack while keeping routine proof search out of submitter turns.

## Changes

  - Clarified novelty-seeking and solution-seeking goals in prompt engineering of proof-solving prompts.
  - Streamlined features UIX interface/control panel.
  - Added state persistence to live activity logs in GUI for each mode between crashes, restarts, and stops/starts.
  - Simplified model roles and condensed all proof-submission roles to one model selection.
  - Renamed High-Parameter Submitter to Rigor & Proofs Submitter and moved critique generation onto that role.
  - Refactored autonomous recommended profile format so standalone critique role entries are removed while legacy saved profiles still hydrate through Rigor & Proofs.
  - Completed deterministic Assistant proof-support ranking/cache hardening with no separate rater function.
  - Softened language on harmless stale tab warning regarding API keys and throttled the log occurance.
  - MinMax M3 replaces Kimi K2.6 as King of The Hill, due to its high knowledge and affordable API cost.
  - For OpenRouter hosts, USA inference host companies now show with an American flag image next to them to help reflect the potential for higher-standard data protection laws.
  - Start/stop research button is now immediately responsive to users input without the prior start up/stop delay.
  - Context overflow stops now idicate the system stopped due to the model running out of limits for the mandatory direct injection context. Some context must be direct injected, such as the brainstorm, otherwise the system would produce misalignment, and other context accumulation errors over long runtimes.
  - OAuth errors are now durable and recoverable on browser disconnect and reconnects.
  - Standardized prompt memory storage across the program to all use the same memory handling.

## Bug Fixes

  - Fixed manual mode prompt persistence so saved prompts are not lost across crashes, restarts, or repeated continue starts.
  - Added backend prompt recovery and clear-only reset handling for durable manual Aggregator and Compiler prompts.
  - Modified X.ai and Codex OAuth attribution from bare "moto" to MOTO Autonomous ASI-specific identifiers.
  - Fixed pruned Stage 2 papers staying visible as dimmed read-only cards instead of disappearing from the live paper grid.
  - Fixed proof-identification model output failures being mistaken for no proof candidates, which could skip proof checking and advance to paper writing.
  - Fixed stale OpenRouter/OAuth copy in provider error messages and README setup docs.
  - Fixed stale LeanOJ proof-search regression coverage to validate Assistant-owned proof support.
  - Fixed proof-search index freshness, disabled-corpus filtering, and active manual proof-check Assistant role preservation.
  - Fixed hosted settings so desktop OAuth status/model endpoints are not polled when OAuth capabilities are unavailable.
  - Fixed Aggregator and Compiler Assistant settings so disabled Agent Conversation Memory makes controls actually disabled, not just visually greyed.
  - Fixed Assistant memory prewarming so eligible producer paths still refresh memory before prompt-size preflight failures.
  - Fixed "settings saved" UIX collision render bug causing small page layout shift on settings update.
  - Change mode panel now is in sync with the workflow tab, stopping premature tab expansions.

  Authored by Patrick White, Patrick@Intrafere.com

Author: Pat

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

@@ -19,11 +19,13 @@ alwaysApply: true
 
 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.
 
+7b.) SyntheticLib4 / unified proof-history search rule updates should stay high-level until the specific build phase lands. Exact JSON prompt schemas and prompt text are updated word-for-word only when the corresponding prompt/tool implementation is undertaken; planning docs alone do not require an API contract bump.
+
 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.
 
 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.
+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 prioritize high-impact prompt-solving targets 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 supporting lemmas, routine helpers, standard Mathlib/textbook facts, minor reformulations/local formalizations, trivial/easy proofs, 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.
@@ -32,9 +34,9 @@ alwaysApply: true
 
 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 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.
+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) and optional metadata-only `search_lean_proofs` context so it can avoid repeating failed edits without turning the master proof into a known-knowledge library. 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` 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.
+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, but brainstorm validation must still reject artifacts that do not directly discharge, split, or repair exact template obligations.
 
 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.
 

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

@@ -63,7 +63,7 @@ All Aggregator offload order and source-exclusion rules are centralized in `rag-
 
 ## Role Selection
 
-User selects model per role. Multiple roles can share a model. Models load with user-set context sizes.
+User selects model per role. Multiple roles can share a model. Models load with user-set context sizes. Aggregator settings also expose one shared `aggregator_assistant` memory-search LLM role for all submitters; built-in/default profiles set Assistant equal to the primary Validator, and Session History Memory disabled greys Assistant out. During manual Aggregator brainstorming and proof checks, Assistant must run in parallel as its own configured model role to refresh the current best up-to-7 verified-proof support pack; local proof search/cache may prefilter candidates, but live support packs require configured Assistant LLM selection. Validator prompts never receive Assistant context.
 
 Per-role Supercharge is optional. When enabled for a submitter or validator, `api_client_manager.generate_completion()` runs 4 parallel full answer attempts for that role call, then a 5th same-model synthesis call and returns only the synthesis result. Supercharge candidate attempts intentionally use temperatures `[0.0, 0.2, 0.4, 0.8]` to diversify parallel outputs; synthesis remains `0.0`. Candidate attempts are sanitized to reusable visible answer text before synthesis; private thought/channel/control transcript text must never be fed back as feedback, brainstorm memory, or synthesis context. The synthesis prompt frames candidates as optional working material: the model may use one, combine several, ignore all, or write a stronger new answer, while preserving the original role output contract. If Boost applies to that role/task, all internal Supercharge calls use the Boost config first. Tool-call requests bypass Supercharge.
 
@@ -81,7 +81,7 @@ When ALL submitters AND validator use the same model → single-model mode:
 
 ## Multi-Submitter Configuration
 
-Per-submitter: provider (LM Studio / OpenRouter / desktop-only OAuth providers such as OpenAI Codex or xAI Grok in default mode; OpenRouter only in generic mode), model, OpenRouter host provider when applicable, LM Studio fallback for cloud providers (default mode only), context window, max output tokens, and Supercharge checkbox. UI: "Number of Submitters" selector (1-10), "Copy Main to All" button.
+Per-submitter: provider (LM Studio / OpenRouter / desktop-only OAuth providers such as OpenAI Codex or xAI Grok in default mode; OpenRouter only in generic mode), model, OpenRouter host provider when applicable, LM Studio fallback for cloud providers (default mode only), context window, max output tokens, and Supercharge checkbox. Assistant has the same provider/context/output setting shape but is not a submitter and is not counted in submitter parallelism. UI: "Number of Submitters" selector (1-10), "Copy Main to All" button.
 
 OpenRouter auto-fill rule: selecting an OpenRouter model auto-fills context from the model-level `context_length`. Max output tokens use `min(20% of model context_length, endpoint max_completion_tokens)`: auto provider mode filters weak/low-cap endpoints and uses the smallest remaining capable endpoint cap, while an explicit host selection uses that host's largest exposed endpoint cap. Endpoint `context_length` / `max_prompt_tokens` rows are diagnostics, not context shrink limits. If endpoint output caps are incomplete, preserve current values (no guessing).
 
@@ -119,6 +119,6 @@ JSON validation failure: reject submission, send reason + content to submitter's
 
 ## Optional Lean 4 Proof Submissions
 
-When `lean4_enabled`, submitters may use `submission_type="lean_proof"` for prompt-directed proof candidates whose claimed novelty is public/citable and absent from standard references or Mathlib, not merely new to the program. Once Lean accepts real proof code, preserve and register it for novelty/triviality ranking even if it proves a narrower supporting lemma than intended; downshift the stored statement instead of discarding it. Hard rejection remains only for non-Lean-verified attempts, malformed submissions, or fake proof devices such as new `axiom`/`constant`/`opaque` declarations.
+When `lean4_enabled`, submitters may use `submission_type="lean_proof"` only for high-impact prompt-directed proof candidates whose claimed novelty is public/citable and absent from standard references or Mathlib, not merely new to the program. The shared Lean proof gate rejects missing/invalid novelty tiers and missing prompt-relevance/novelty/anti-standard-result rationales before Lean cost. Supporting lemmas, routine helpers, local facts, trivial/easy proofs, and weakened substitutes are not valid targets. Once Lean accepts real proof code, preserve/register the actual artifact for novelty/triviality ranking, but normal brainstorm validation may still reject it from the accepted-submission database when the actual theorem is low-impact, trivial, routine, or redundant. Hard rejection always applies to non-Lean-verified attempts, malformed submissions, or fake proof devices such as new `axiom`/`constant`/`opaque` declarations.
 
-Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It uses standard proof discovery, asking for candidates that directly solve the user prompt first and then candidates that substantially build toward solving it. Any non-duplicate Lean-verified proof from that user-triggered check is stored in the active manual proof database and appended to the active manual Aggregator database proof appendix for user-visible display/download, regardless of novelty rating; progress is also persisted to the manual Aggregator event log so live activity can recover missed WebSocket events. Later proof-check prompts strip that generated-proof appendix and receive verified proofs through the manual proof database injection instead. Manual Aggregator clear archives the active manual proof database to history and resets active proof context to empty; clear is rejected while manual proof verification is active.
+Manual Aggregator live results expose "Try to Prove This" over the current accepted-submissions database. It uses standard proof discovery, asking for candidates that directly solve the user prompt first and then candidates that substantially build toward solving it. When Session History Memory is enabled, the separate Assistant LLM role runs in parallel during brainstorming and proof checks, maintaining a freshness-tagged up-to-7 pack of fully Lean-verified local/SyntheticLib4 memory supports for eligible submitter/proof roles; proof discovery/formalization may use the latest pack but must not wait for it. Validators never receive Assistant context. Any non-duplicate Lean-verified proof from that user-triggered check is stored in the active manual proof database and appended to the active manual Aggregator database proof appendix for user-visible display/download, regardless of novelty rating. This known-proof preservation is intentional for RALPH looping: the user can see validated work, and later proof checks can avoid redoing exact verified proofs instead of losing them because they ranked `not_novel`. Progress is also persisted to the manual Aggregator event log so live activity can recover missed WebSocket events. Later proof-check prompts strip that generated-proof appendix and receive verified proofs through the manual proof database injection instead. Manual Aggregator clear archives the active manual proof database to history and resets active proof context to empty; clear is rejected while manual proof verification is active.