Quickstart

Ansätze, at ansatze.ai, brings mathematical questions, proving engines, and the evidence behind their results into one workspace. By default every run uses the Ansatz CGM pipeline: a strategist plans, workers prove lemmas, an independent verifier checks each lemma, and a curator scores the search. This guide covers your first run and the tools you can explore afterwards.

1. Open the console

Choose Use as guest to try the console without creating an account. Accounts are created by the site operator; registration is not open to the public. If you have an account, use Sign in with your email and password.

A guest’s run history is tied to a 24-hour session cookie in that browser. Clearing cookies or site data, or moving to another browser or device, loses access to that guest history. Guest work is not transferred when you later sign in, so sign in before starting work you need to retain with an account. Ending the guest session deletes its saved provider key.

If you forget your password, choose Forgot password? on the sign-in page. Use only the newest reset email; a reset link is single-use.

2. Choose how runs are billed

Guest mode defaults to Ansatz CGM · Kimi K3, the tool-free CGM pipeline running on Kimi K3. If hosted Kimi access is available, you can start immediately. Otherwise, open Settings and add your own Kimi API key. The tool-free Plain baseline is also available when enabled by the deployment.

The default guest allowance is 10 total run starts in the browser session, with up to six starts per hour. Deleting a run does not restore a start. After the tenth start a guest session cannot start more runs; a deployment may offer a lower allowance. Guest runs use a smaller CGM budget (fewer model calls, workers, and repairs per run), and guest Lean and DAG actions have an hourly limit. When a limit is reached the console says so and tells you when to try again. Key verification allows six attempts per guest per hour by default.

Claude Code and Codex require sign-in, even when guest starts remain. Their cards stay visible in the dashboard so you can see the available options. Signed-in accounts can run the same CGM pipeline on their own route with Ansatz CGM harness.

Signed-in accounts can use the provider routes enabled by the deployment:

• Add your own provider API key.
• Connect a supported subscription account when that option is available.

Provider keys saved through the console are encrypted at rest in the associated user record. In a guest session, those settings remain tied to the same browser cookie and can become inaccessible if that cookie is lost. Use a signed-in account for durable provider settings. The console selects the credential route associated with the model you choose and limits the normal child-process environment to that route. Signed-in local proving engines share the host's operating-system trust boundary; they are not a sandbox for untrusted code.

3. Start a problem

1. Enter a mathematical statement, or open Open Problems, read its statement and cited progress, and select Click to solve. This prepares the workspace; it does not start a run automatically.
2. Pick an available engine and model. Guests start with Ansatz CGM · Kimi K3 selected; the CGM engines are listed first.
3. Signed-in users can set the iteration budget and optional delegation choices.
4. Select Prove →.

The run opens in its workspace. Read the developing proof in Sandbox, inspect the Conversation, or open Monitor to follow the engine’s activity.

4. Review and continue

A CGM run writes its proof to proof.md together with its fact graph and search record. When the verifier accepts the target theorem, the proof is assembled only from accepted lemmas; otherwise the best candidate is published and marked as not verifier-accepted. Review the argument together with the verifier's verdicts and any open goals.

• DAG → Informal · CGM is the headline view. Facts shows the accepted lemmas and their dependencies. Explore shows the search: plans, subgoals, worker attempts, verifier verdicts, obstacles, dead ends, and the curator's status and score for each node. Select a node to read its statement, proof excerpt, curator comment, and links.
• DAG → Outline is an informal outline of the final proof; for CGM runs it is derived directly from the fact graph. Formal · Lean and Compiler facts show the structure of the Lean file.
• Lean Verification shows the Lean source and checker results. Guests can run Verify, Compile, Check, and Audit, and send feedback, within the guest limits. The coding-agent Harness requires sign-in.

Signed-in users can add focused feedback and continue the same proof run. A guest's main proof run finishes after its pipeline; the guest can still inspect its evidence and use the available Lean actions. A proposed proof, a verifier-accepted lemma, a compiled file, and a verified Lean statement have different meanings—read the reported status and remaining gaps.

How a CGM run works

The Ansatz CGM pipeline is tool-free: each stage is a single model response, and the console's own code enforces the budget, the output format, and the dependency rules.

1. Strategist. Reads the problem and proposes up to a few plans. Each plan names a technique (for example a direct proof, an invariant, an extremal argument, or a reduction) and may split the goal into subgoals that must all be closed (an AND group).
2. Workers. Each worker follows one plan and writes numbered lemmas and a final theorem, each with a statement and a proof that cites only earlier lemmas.
3. Independent verifier. Every lemma is checked in its own fresh model call that sees only that lemma and the statements of the lemmas it cites. A lemma that fails gets a bounded repair attempt; only accepted lemmas become facts.
4. Curator. Scores and annotates the exploration graph, marking goals as open, active, blocked, dead, or closed. Closure through AND groups is computed by code, not by the model.
5. Formal stage. The Lean pipeline fixes the formal statement first, then proves it, and reports compile and axiom checks.

What the labels mean:

• Model-verifier accepted means another model call judged the lemma's proof correct. It is useful evidence, but it is not a Lean certificate.
• Verified in Lean Verification means the Lean checker accepted the file with no sorry and only standard axioms, and no statement-fidelity check flagged a major mismatch with the problem. The fidelity audit is itself a model check and does not run on every action, so still read the formal statement. Compiles — wrong statement means the file checks but proves something other than the problem. A minor fidelity flag, such as a 1 ≤ n hypothesis when the problem says "every natural number n", is shown as a caveat and gets one statement-fix attempt; it never changes the status by itself.
• The Explore graph records the search. Its edges are not proof steps.

The CGM prompts and data formats are adapted from the Ansatz continual-graph-memory project by FrenzyMath, used under the Apache License 2.0; the console's runner and graph validator are original code.

Keep your account safe

• Do not paste API keys into problem statements or chat messages.
• Do not share password-reset links; the token grants temporary access to reset your password.
• Sign out on shared computers.
• Rotate a provider key immediately if you believe it has been exposed.

Proving engines

Availability depends on the deployment and the account’s connected providers. Each run has its own workspace.

Engine	Workflow
Ansatz CGM · Kimi K3	The CGM pipeline (strategist → workers → independent verifier → curator) on Kimi K3, tool-free; the default for guests. Publishes Facts and Explore graphs.
Ansatz CGM harness	The same CGM pipeline on a signed-in account's own Codex, Claude Code, or API route.
IMProof	An author–critic proving workflow based on ProofStack.
Hermes	An embedded agent harness for reasoning and tools.
DeepAgents	A LangGraph agent with a dedicated runtime.
Meta-Harness	A solver, evaluator, and proposer loop.
OpenClaw	An embedded local agent.
Codex, Claude Code / OpenClaude, OpenHands	Coding-agent integrations when available. Claude Code and Codex require sign-in.
Plain	A single-model-call baseline.

Trace views and proof graphs

The monitor records agent activity, token usage, and cost as the run progresses:

• Map view shows a free-form graph of agent activity.
• Pipeline view groups that activity into the workflow’s stages.
• The workspace’s DAG tab opens on Informal · CGM (Explore and Facts). Other harnesses show their execution trace there; Outline, Formal · Lean, and Compiler facts show the informal outline and the Lean structure.
• Lean Verification records source, compilation or checking results, and any remaining proof gaps.

Use the graph to understand dependencies and the checker output to inspect formal evidence. An edge in a graph alone does not certify a mathematical argument.

Reusable memory, skills, and tools

Signed-in workspaces can use a shared library to carry useful material into future runs:

• Memory keeps context and summaries from earlier work.
• Skills provide reusable strategies and instructions.
• Tools provide executable scripts to compatible engines.

Enabled library items are copied into a run’s _library/ directory and included in its prompt context. A library is reusable context; a run’s workspace preserves that run’s artifacts and evidence.

Project layout

For developers working with a local checkout:

agent_monitor/          # Console, runners, and orchestration
monitor_core/           # Dashboard and token/cost tracking
engines/                # Embedded engines and their environments
problems/               # Local mathematical statements
data/                   # Runtime runs, logs, caches, and library

Keep exploring

• Browse Open Problems for a sourced question to investigate.
• Explore the research DAG and inspect a worked example.
• Read News for mathematical developments, model releases, and research updates.
• See Engineering & reliability for implementation details.