MOTO v1.1.08

[Intrafere]

MOTO v1.1.08

Features

• Added standalone-versus-group proof novelty rankings with combined claims and exact member proof IDs.
• Added separate Lean source and ranked-group JSON downloads across current and historical proof views, including LeanOJ.

Changes

• Propagated grouped novelty provenance through canonical storage, versioned proof-search indexing/hydration, APIs, notifications, and live activity.
• Made group membership self-contained, same-run-only, pruning-aware, and atomic in model context; incomplete groups are omitted instead of being presented as standalone discoveries.
• Reworked Codex Responses as incremental SSE with strict terminal completion, typed failures, sequential recovery, and a non-canceling 25-minute watchdog.
• Added shared provider-recovery handling so timed usage windows cooldown-retry across providers, while untimed spending or entitlement stays repair-required.
• Gave xAI Grok the same stop-aware timed-cooldown and success-confirmed resume path as Codex and Sakana, using JSON body reset or ordinary 429 Retry-After, never treating spending-limit headers as a reset.
• Standardized settings descriptions across all three modes to use non-italic text.
• Made startup-provider and legal-disclaimer dialogs responsive, viewport-bounded, and visibly scrollable only when needed.
• GPT 6.1 Sol replaces GPT 6 Sol as King Of The Hill.
• Hardened credential setup with provider-scoped autofill-safe inputs, authenticated OpenRouter status, and transactional desktop key/OAuth persistence.
• Added xAI OAuth reasoning-effort controls across Aggregator, Compiler, Autonomous Research, and LeanOJ settings, with Auto/high/medium/low/disabled choices.
• Made continuous “Try to prove this” runs report each no-discovery round and finish normally after 10 consecutive rounds without candidates, resetting the streak whenever candidates are found.
• Replaced the 75% pre-Lean proof-list novelty gate: any list with at least one Validator-approved novel candidate now proceeds with only those candidates, and lists regenerate with feedback only when none are novel.
• Made novelty the only admission gate across proof discovery, proof and brainstorm Validators, topic selection, completion review, and paper continuation: whole-question attacks still come first, but genuinely novel incremental or indirect progress toward the user prompt is now accepted instead of rejected as tangential or non-essential.
• Made proof-target selection budget-aware: discovery now states the real 5-attempt Lean budget (3 full-proof, then 2 tactic-script attempts), prioritizes direct solutions whenever they have a reasonable chance of being fully proved within it, and otherwise selects the strongest genuinely novel piece or indirect step that can be proved, without lowering the novelty bar; removed the stale promise that formalization would narrow oversized targets, and aligned compiler rigor discovery.
• Routed failed proof targets through discovery instead of blind retries: discovery now sees each source brainstorm's unresolved failed targets, follow-up rounds no longer re-propose a failed target unchanged, and completed Autonomous papers no longer re-run every failed brainstorm target unchanged with 5 fresh attempts. Discovery decides whether to retry with a materially different formalization, prove a novel piece, or move on; an optional validated retry link resolves or updates the original target.
• On Windows, when MOTO's folder is too deep for Mathlib, Lean's workspace now lives in a short per-user folder (%LOCALAPPDATA%\MOTO\lean) and the launcher deletes the unusable in-folder copy; proofs are disabled with "move MOTO to a short folder" guidance only if that isn't possible.
• A broken Lean setup now stops the workflow with a durable "Lean 4 setup needs repair" message and keeps the proof checkpoint, so pressing Start resumes the same proofs; each proof round, rigor cycle, and final-solver attempt first gives a failed setup one fresh attempt.
• Bumped the API contract to build6-v121 for the new lean_workspace_repair_required event and terminal reason.

Bug Fixes

• Preserved completed Codex responses across broken HTTP framing and prevented terminal-less streams or nested retries from causing false success and request multiplication.
• Added bounded, secret-redacted provider errors, retry timing, and unknown-outcome details to Live Activity.
• Prevented group-level discovery tiers from being presented or injected as standalone theorem discoveries.
• Preserved group rankings during duplicate detection and rejected cross-run members in archived group exports.
• Preserved group provenance through proof-search rebuilds and suppressed incomplete group-ranked Assistant support.
• Restored group exports from canonical same-run proof storage after interrupted LeanOJ state publication.
• Added accessible archived-download errors and viewport-bounded scrolling for proof discovery notifications.
• Prevented novelty context overflow from silently changing a group-capable ranking into a standalone-only judgment.
• Preserved proof-specific output-truncation recovery for Codex max_output_tokens responses.
• Grounded proof novelty rankings in the mathematical result actually established by Lean-verified code, rather than surrounding target claims, while preserving group-scoped ranking and adding visible novelty-assessment start activity.
• Prevented startup dialogs from clipping off-screen; overflow now gets a slow one-time assist that permanently stops after user interaction or under reduced-motion settings.
• Prevented invalid or stale OpenRouter keys and OAuth-only providers from falsely satisfying startup readiness.
• Prevented credential replacement, clear, autofill, and OAuth callback failures from leaking transient secrets, splitting runtime/keyring state, or discarding retryable login state.
• Prevented xAI spending-limit Retry-After headers from becoming timed resets, and prevented ordinary xAI 429 Retry-After windows from burning adapter retries instead of entering cooldown.
• Hardened Lean setup with probe-verified Git auto-installation and an authoritative Git/Lean/Lake capability gate that persisted settings cannot override.
• Prevented submitter-count resets, stale role auto-fill overwrites, and legacy submitter-ID failures in Aggregator and Autonomous settings.
• Prevented rejected proof-list regeneration from looping indefinitely on valid no-candidate results; empty rounds now use the existing Live Activity format and count toward normal 10-round completion.
• Retried successful but malformed OpenRouter responses with missing, empty, or invalid completion choices before workflow backoff; preserved typed transient and context-limit handling across Compiler, Autonomous proof checkpoints, and manual “Try to prove this” runs so provider failures cannot become semantic rejections or opaque local retry stalls.
• Prevented live-context proof pruning from leaving stale verified-proof blocks in an active proof round; subsequent candidate discovery, regeneration, formalization, and checkpoint continuation now rebuild owning-run proof context from the current proof-set revision without altering in-flight model calls.
• Resolved the frontend npm audit warnings shown at launch by updating KaTeX to 0.19.0 (GHSA-238p-pmpm-9mq7) and source-map-js to 1.2.2 (GHSA-68fv-2mgg-jv7q) in the lockfile, and updated rendered-math styling for KaTeX's renamed classes.
• Fixed OpenAI Codex turns longer than 15 minutes never completing: the Codex backend closes HTTP/SSE streams at roughly 900 seconds, so Codex completions now stream over the Responses WebSocket transport used by the Codex CLI, falling back to SSE only when the handshake is rejected; Live Activity names the transport on each retry.
• Fixed proof-check Live Activity going silent after a browser tab froze, was discarded, or reloaded: proof runs now number their activity in a bounded backend journal, and the tab replays only the events it missed after reconnecting or resuming, without duplicates or changes to run status.

Developer Features

• Modernized the removable cross-field workflow testing overlay with production-backed lifecycle, pruning-preservation, live activity log checks, and automatic proof-round coverage.

• Added fail-closed SyntheticLib compatibility evidence with canonical receipts, contract tests, and isolated local release verification.

• Hardened SyntheticLib contract evidence with exact unpublished-state validation, rollback-safe publication, non-destructive retained output, and expanded semantic-forgery regression coverage.

• The program now adopts .claude modularized rules format for Claude Code users instead of .cursor rules format for Cursor users. If needed, the rules can be easily converted by any forks or local developers.

  Authored by Patrick White, Patrick@Intrafere.com