MOTO at a Glance

MOTO combines a Python research backend, a browser-based interface, live activity updates, local persistent storage, and configurable access to local and cloud models. For changing technical details, consult the versioned launcher code, dependency manifests, update manifest, and repository documentation for the installed commit. If prose and implementation conflict, the versioned code and manifests take precedence.

• Autonomous Research: topic exploration, validated brainstorms, multi-paper research, optional proof checkpoints, and optional final synthesis.
• Advanced Manual Research: direct control over the Aggregator prompt, Compiler prompt, model roles, output types, and research context.
• Configurable model team: multiple submitters, a validator, writing and rigor roles, and optional proof-history assistance.
• Provider flexibility: local LM Studio models, OpenRouter models, and supported desktop subscription or API providers for selected roles.
• Formal proof tools: optional theorem identification, Mathlib search, Lean 4 verification, Z3 hints, proof history, dependency metadata, downloadable Lean source, and application-generated JSON proof records.
• Durable work: saved brainstorms, papers, proofs, final answers, critiques, logs, and workflow checkpoints.

How MOTO Explores a Problem

1. Diverse submitters explore candidate solution paths

MOTO can run multiple submitter roles. Each role can use its own provider, model, context budget, output budget, reasoning setting, and optional fallback. When the selected runtime permits genuine concurrency, submitters work in parallel; shared local-model constraints can cause sequential operation instead.

Intrafere calls this broader strategy Top-P Exploration through structured brainstorming and validated feedback. This names the orchestration method: repeated generation against an evolving knowledge base, varied exploration roles, validation, rejection feedback, and recombination. It should not be confused with direct control of an API’s standard top_p sampling parameter.

2. One validator controls acceptance

Submitter proposals enter a shared queue and are evaluated by one sequential validator role. The validator judges whether a proposal advances the user’s objective, adds useful information, avoids unsupported claims, and contributes something not already represented in the accepted database. Rejected proposals return with feedback, and each submitter retains its recent rejection history to guide later attempts.

“Validated” means filtered by the configured AI validator; it does not mean independently fact-checked, peer reviewed, experimentally reproduced, or formally proven.

3. The accepted database is periodically refined

As accepted knowledge grows, MOTO can run cleanup reviews. The validator may propose redundant or contradicted material for removal and review that proposal before changing the active database. Approved removals are also removed from the accepted-knowledge retrieval index.

4. A progressive solution path can guide later work

As accepted research accumulates, MOTO can maintain a durable Progressive Solution Path for the run. Validators may propose an initial route or material revisions, but a designated submitter reviews proposals before they become the canonical advisory path. When it fits the available context, the approved path can guide eligible later producer and solver calls. Its revision and proposal state are visible in the Workflow panel. It is AI-generated planning guidance, not a guarantee that the route is correct or complete.

5. Large context is allocated deliberately

Mandatory instructions and critical source material are directly injected when required. Other accumulated material can use staged retrieval combining query preparation, lexical and vector recall, diversification, and token-budget packing.

Retrieval is selective. A very large source library is not necessarily visible in full during every model call, and mandatory content that cannot fit can stop the affected stage with a visible context-overflow error rather than being silently discarded.

Autonomous Research: The Three Tiers

Tier 1 — Topic selection and brainstorm aggregation

MOTO explores candidate research questions, selects a topic, validates that choice, gathers relevant prior work, and runs the Aggregator. Completion review occurs as accepted knowledge grows, and the workflow can move to paper writing when completion logic or the operator requests the transition.

You can monitor accepted and rejected work, stop the run, clear it, or force the current brainstorm into paper writing. Autonomous state is saved so many interrupted runs can resume from their recorded tier and phase.

Tier 2 — Iterative paper construction

The Compiler creates and refines an outline, writes the body, runs critique and revision, writes the conclusion, writes the introduction after the main content exists, performs a pre-abstract review, and writes the abstract last. A single brainstorm can produce as many as three related papers when the continuation decision supports further development.

Earlier active papers can become references for later work. Redundancy review may prune a paper from future model context while preserving it in Completed Works for reading and download.

Tier 3 — Optional final-answer synthesis

Tier 3 is an optional final-synthesis workflow. MOTO can consider whether enough research exists for synthesis, or the operator can request final synthesis after completing current work or from completed papers only.

Final synthesis assesses certainty and can produce a short-form answer or an organized long-form volume. The volume path can arrange existing papers as chapters and write needed introduction, conclusion, or gap chapters. Because synthesis compounds claims from multiple AI-generated papers, it should be used with particular scrutiny.

Advanced Manual Research

Step 1 — Build knowledge with the Aggregator

1. Open Advanced Manual S.T.E.M. ASI and select Aggregator.
2. Enter a focused research prompt. You can append text or Lean content and attach multiple context files.
3. Configure the available submitter roles, the validator, and optional research-memory assistance.
4. Select models, providers, context windows, output limits, reasoning settings, OpenRouter hosts, and fallbacks as needed.
5. Select Start Aggregator, then monitor Live Results, logs, queue activity, token use, and validator feedback.

Step 2 — Construct the paper with the Compiler

1. Open Compiler and enter separate instructions describing the paper or solution report to build from the accepted Aggregator database.
2. Configure the Validator, Writing Submitter, and Rigor & Proofs Submitter. Agent Conversation Memory can add Assistant proof-history support.
3. Allow Research Papers, Mathematical Proofs, or both. At least one output type must be enabled.
4. Select Start Compiler and follow the paper in Live Paper.
5. Save a draft, stop and save, reset the paper, request a critique, try formal proof generation, or export raw text and PDF.

Manual Aggregator and Compiler prompts are intentionally separate. This gives the operator control over what knowledge is explored and how that knowledge is transformed into a final document.

Optional Lean 4 Proof Verification

When Mathematical Proofs are allowed and Lean 4 is available, MOTO can inspect completed brainstorms and papers for theorem candidates. Autonomous Research also makes a one-time AI proof-framing decision about whether to add proof-oriented guidance to the research prompt; that framing decision does not disable later candidate checks.

MOTO searches local Mathlib information, generates Lean code, and can retry formalization with Lean diagnostics as feedback. It rejects placeholders such as sorry and admit and checks for disallowed newly introduced declaration devices. Context overflow is treated as an operational deferral rather than evidence that a theorem is false.

For selected arithmetic-looking candidates, an AI model may translate a claim into SMT-LIB for optional Z3 analysis. Only an unsat result supplies suggestions to a later Lean attempt. sat, unknown, translation errors, and solver failures neither prove nor disprove the intended theorem. Only Lean acceptance is treated as formal verification.

Lean verifies only the formal declaration accepted by the configured Lean and Mathlib environment. It does not verify the surrounding paper, empirical claims, natural-language interpretation, usefulness, or novelty. MOTO may normalize code fences and imports before checking the generated declaration.

After Lean accepts code, an AI classifier compares the accepted declaration with the intended theorem. If it identifies a weaker or different result, MOTO preserves the proof under the extracted Lean statement and records the mismatch. If alignment classification is unavailable, malformed, or over context, the Lean-accepted proof is still preserved with alignment marked unavailable. Inspect the exact declaration and alignment metadata rather than treating the original natural-language candidate as verified.

Novelty labels are AI assessments, not exhaustive literature or priority determinations. Unusable novelty output falls back conservatively, and exact canonical matches from other runs can be categorized as duplicate occurrences.

Dependency views are heuristic provenance aids, not complete Lean dependency graphs. Implicit, unqualified, elaborated, tactic-internal, and transitive dependencies may be absent, and dependency extraction failure does not invalidate a Lean-accepted proof.

The local proof library supports active and archived work, text search, and novelty-category filters. Federated proof search can query enabled local Autonomous Research, manual, and Proof Solver history with a Verified-only option. SyntheticLib4 integration is currently marked coming soon; it participates only when an authorized local snapshot is explicitly installed and enabled. Repository fixtures support development and tests but are not a live public corpus. MOTO can export exact generated .lean source and application-generated JSON proof records containing provenance, hashes, environment metadata when available, novelty assessments, solver hints, and dependencies. These records are unsigned exports, not cryptographic attestations.

Assistant Session History Memory

Assistant Session History Memory—shown under Connectivity as Agent Conversation Memory—is a non-blocking verified-proof retrieval system, not a general chat transcript. When enabled, it can search eligible prior Autonomous Research, manual, and Proof Solver records and prepare relevant supporting context for later producer calls without making the main workflow wait.

Validators and critique stages do not receive Assistant memory. The requesting run’s current active proof corpus is excluded from historical-memory search. Disabling Agent Conversation Memory stops new Assistant searches and clears active result packs and cooldown state without deleting canonical completed proofs or research history.

Before You Install

Runtime requirements can change as dependencies evolve. Confirm the launcher checks, dependency manifests, update manifest, and repository documentation for the installed commit. If prose conflicts with launcher behavior, treat the versioned launcher and manifests as authoritative and report the documentation mismatch.

• Python and Node.js: install compatible versions listed in the repository README. The launchers check these runtimes before startup.
• Provider path: LM Studio with chat and embedding models, or an OpenRouter API key.
• Internet: required for initial packages, cloud providers, update checks, and first-time optional tool downloads.
• PDF export: requires Playwright Chromium and compatible system libraries.
• Lean proofs: require working lean and lake commands. The launcher uses elan as its preferred installer and toolchain manager when Lean is missing. Initial Mathlib setup needs Git, internet access, time, and several additional gigabytes.
• Z3: optional and used for hints only; Lean remains the proof authority.
• Wolfram Alpha: an App ID is needed only if you choose to enable its optional Compiler construction tool.

Windows 10+ and Ubuntu 24.04 have dedicated consumer launchers. Ubuntu 24.04 is the tested Linux launcher target. Other Linux distributions and macOS may work through compatible manual installation, but they do not have the same tested one-click launcher support.

Windows One-Click Installation

1. Open the MOTO repository on GitHub and select Code → Download ZIP, or clone the repository with Git.
2. Extract the complete folder to a writable location such as your Desktop.
3. If using LM Studio, start its local server and load nomic-ai/nomic-embed-text-v1.5 plus at least one chat model. Otherwise, have an OpenRouter API key ready.
4. Double-click Click To Launch MOTO.bat.
5. Allow the launcher to complete Python, frontend, Playwright Chromium, Lean/elan, and Z3 setup. These downloads can take time. When Lean is enabled, the backend begins preparing the Mathlib workspace in the background during startup; proof and proof-status requests may wait for the same potentially lengthy update and cache download.
6. When the browser opens, acknowledge the disclaimer and configure OpenRouter or confirm the prepared LM Studio connection.
7. Open Settings, select a recommended profile or configure your own model team, enter a research objective, and select Start Research.

What the Windows launcher does

• Finds a compatible Python installation and can attempt to install a supported Python runtime with winget if none is available.
• Finds compatible Node.js and npm and can attempt a winget installation or upgrade.
• Checks GitHub main for a newer supported build before normal startup.
• Installs or updates Python requirements and frontend packages.
• Installs Playwright Chromium on a best-effort basis for PDF export.
• Finds or attempts to install optional Lean 4 and Z3 tools without making ordinary research startup depend on them.
• Checks LM Studio and desktop keyring readiness.
• Generates a matching local backend/frontend API token, starts both services, waits for readiness, and opens the UI.
• Makes a best-effort Windows request to prevent idle-triggered automatic sleep while a top-level workflow is active, then releases that request when it stops. Failure to establish the native power request does not stop research, so verify Windows power behavior before relying on unattended runs. The request does not block display sleep, explicit sleep, hibernation, shutdown, or critical-battery actions.

Windows uses the compatible Python installation the launcher finds; it does not automatically create a Windows virtual environment. The Ubuntu launcher does create a repository-local virtual environment.

Ubuntu 24.04 Launcher Setup

Before launch, install the operating-system packages required by the versioned launcher and dependency manifests. These include a compatible Python runtime with venv support, Bash, compatible Node.js and npm, Git, and curl. Playwright may also need distribution browser libraries. A Secret Service-compatible desktop keyring is needed to save and restore desktop provider credentials reliably.

1. Download and extract the repository, or clone it with Git.
2. Open a terminal in the repository root.
3. If using LM Studio, start its server with the Nomic embedding model and at least one chat model; otherwise, have an OpenRouter key ready.
4. Run bash linux-ubuntu-launcher.sh.
5. The wrapper creates or reuses .venv and delegates to the shared Python launcher.
6. Complete provider setup in the browser and select a model profile.

What the Ubuntu launcher does—and does not do

• It verifies that a compatible Python command exists and creates a repository-local .venv.
• It uses the same dependency, update-check, optional Lean/Z3, service-readiness, and browser-opening orchestration as Windows after Python starts.
• It opens backend and frontend in supported desktop terminal emulators when available. In a headless or unsupported terminal environment, it runs them in the background and writes launcher_backend.log and launcher_frontend.log under the active log root.
• It does not install Ubuntu’s Python, python3-venv, Node.js, npm, Git, curl, keyring service, or Playwright operating-system libraries through apt. Install those system prerequisites separately.
• If no compatible Linux desktop keyring is available, MOTO can still start and LM Studio-only use remains possible. Saving or restoring desktop API keys and OAuth credentials can fail until a working keyring is installed, unlocked, and available in the same desktop session. MOTO does not intentionally fall back to plaintext credential files.

Updates, Runtime Identity, and Saved Work

Both launchers check the official GitHub main branch for a newer build identity. Official main checkouts tracking the official origin/main can apply supported fast-forward updates when launcher-managed services are closed and no tracked files are modified. Nonstandard, tracked-modified, ahead, or diverged Git checkouts remain runnable but are detection-only. Untracked files are not considered by this cleanliness check; review local untracked files before updating if they could affect application behavior.

Extracted ZIP installations can also be updated, but without Git metadata the updater cannot identify local source-code modifications. An accepted ZIP update copies target-commit files over the installation while skipping documented preserved state paths. Matching local application files are overwritten, but files absent from the target archive are not deleted, so stale or custom files can remain. Back up the installation—or replace it with a fresh extraction—when an exact target-commit tree is required.

Update preservation covers the active data and log roots, virtual environments, frontend modules, local environment files, launcher instance metadata, browser-storage identity, and operating-system keyring identity. The frontend dependency audit is read-only: high-severity findings produce a warning so maintainers can ship a tested lockfile update; the launcher does not run npm audit fix.

Automatic updates trust HTTPS responses and repository metadata from the official GitHub project. The updater uses commit-addressed archives and rejects path traversal, but it does not currently verify a detached release signature or an independently published archive checksum. Security-sensitive installations should review the target commit and update diff before accepting an update.

The launcher also installs and executes third-party components, including Python and npm packages, Playwright Chromium, elan/Lean, Z3, and Mathlib tooling. Some downloads are selected from current upstream releases without an independently pinned checksum or detached signature; on Linux, missing elan is installed through the upstream GitHub installation script. Review these upstreams and installation commands before using MOTO on a security-sensitive host, and use an appropriately isolated environment when stronger supply-chain assurance is required.

A normal launch maintains a stable default browser origin, data root, log root, and credential identity so saved work and settings remain attached to the same installation. Port conflicts are handled conservatively to protect that identity. Parallel isolated instances require advanced, explicit instance, storage, namespace, and port configuration; see the repository for the current runtime contract.

Troubleshooting

The launcher cannot find Python or Node.js

On Windows, run Click To Launch MOTO.bat again and allow its winget attempts. If automatic installation is unavailable, install the Python and Node.js versions listed in the repository README, then restart the launcher. On Ubuntu, install compatible Python, venv support, Node.js, and npm through your normal system package or runtime-management method before running the shell launcher.

MOTO cannot confirm LM Studio

Start the LM Studio local server and load the chat and embedding models required by the installed build. The launcher first checks whether LM Studio responds. After the backend and interface start, MOTO separately reports available models and tests embedding readiness. Workflow start is blocked when no supported embedding path is ready; also confirm that each selected chat role has a usable chat model.

The default frontend port is already in use

Close the existing MOTO frontend or the other process identified by the launcher. A normal launch intentionally preserves its browser origin because changing it can separate the session from browser-saved settings and prompts. Advanced isolated instances require explicit configuration.

A model returns malformed or truncated JSON

Review logs, increase that role’s output budget when the response is genuinely truncated, reduce excessive context where appropriate, or switch model or OpenRouter host. Provider timeouts, rate limits, exhausted credits, and malformed model output can pause or delay long-running work.

A mandatory prompt exceeds the model context window

Increase the affected role’s context window, reduce its reserved output budget when safe, or reduce the mandatory source size. MOTO deliberately refuses to truncate some proof and workflow-critical inputs.

PDF export is unavailable

Re-run the launcher and inspect its Playwright warning. On Linux, install Playwright’s required operating-system libraries. Ordinary research and raw-text export can continue without PDF support.

Lean or Mathlib setup is incomplete

Confirm Git and internet access and leave several gigabytes free. The launcher prepares Lean, and the backend begins preparing the Mathlib workspace in the background when Lean is enabled. This can run a long lake update and precompiled-cache download with no fixed timeout. Proof requests wait for workspace preparation and may trigger or retry it if startup preparation has not completed. If Lean remains unavailable, disable mathematical proofs and continue with brainstorm and paper outputs.

ChromaDB reports corruption

MOTO treats chroma_db as a rebuildable retrieval cache and performs automatic maintenance; Windows desktop runs may quarantine prior-process cache state and rebuild it. If corruption persists after a clean restart, stop all MOTO services, back up the active data root, remove only its chroma_db cache folder, and restart. Do not delete the rest of the data root unless you intend to remove saved work.

A provider key will not save on Ubuntu

Confirm that a Secret Service-compatible keyring is installed, unlocked, and available in the same desktop session that launched MOTO. Restart the launcher after enabling GNOME Keyring or another Python-keyring-compatible Secret Service backend.

Responsible Use and Verification Boundaries

• MOTO’s papers and brainstorms are AI-generated and may contain incorrect, incomplete, misleading, or fabricated claims.
• Validator acceptance is an AI judgment, not independent peer review or external fact-checking.
• AI-assessed novelty does not establish global originality, publication priority, or patentability.
• Lean acceptance verifies the formal declaration in the prepared source checked by Lean—not the entire paper or necessarily the initially intended natural-language theorem.
• A failed formalization does not show that a theorem is false; the search, model, context, timeout, or library may simply be insufficient.
• MOTO executes AI-generated Lean source through the local Lean and Lake toolchain. Its proof-integrity checks reject selected shortcuts, but they are not an operating-system sandbox. Use a normal non-administrator account and avoid running untrusted proof work on a sensitive host.
• RAG retrieves selected evidence under a token budget and does not expose the entire source library to every call.
• Long autonomous runs depend on provider availability, credits, rate limits, local stability, storage, and model behavior.
• Research artifacts, uploads, logs, databases, workflow state, proof metadata, and generated .lean files are stored locally in ordinary files and are not encrypted by MOTO itself. Clearing manual work may archive verified proofs rather than erase them.
• Desktop provider API keys and OAuth token bundles are stored through the operating-system keyring rather than intentionally written into research artifact files. Their confidentiality and availability depend on the operating system and active keyring backend.
• Cloud-selected roles can send prompts and context to third-party providers. Fully local privacy requires local chat and embedding paths with cloud fallbacks and external integrations disabled.
• A normal desktop launch binds the backend to localhost. Advanced host overrides can bind it to another network interface; do not use them to expose the desktop backend directly to an untrusted network. The desktop runtime is not a hardened public deployment.
• The generated proof workspace fetches Mathlib through Lake rather than pinning Mathlib in the application repository. Preserve exported environment metadata and workspace manifests when strict reproducibility matters.

Treat MOTO as a research prototype and an instrument for structured exploration. Independently verify important mathematical, scientific, engineering, medical, legal, financial, safety-critical, or policy conclusions with qualified reviewers and appropriate external evidence.