Ansätze

Appearance

UCLA · AI + MATHEMATICS

AnsätzeEvery proof begins with an idea.

An AI workspace for mathematical research at ansatze.ai. By default, each run plans, proves, and independently checks its lemmas with the Ansatz CGM pipeline, then shows the evidence as graphs you can inspect and a Lean stage you can run.

Use as guest
Sign in
Quickstart
Decorative mathematical illustration of a curved surface and connected ideas.
UCLA Samueli Computer ScienceUCLA Samueli Computer ScienceUCLA College Physical Sciences MathematicsUCLA College Physical Sciences Mathematics

THE RESEARCH ATLAS / INFORMAL ↔ FORMAL

Two languages.
One mathematical landscape.

Explore mathematical statements alongside their connected Lean declarations, across 60 projects. Select an idea, read its source, and follow the formal reference.
24,950 informal entries · 16,682 formal declarations
16,761 supplied cross-links
INFORMAL ↔ FORMAL16,761 LINKS ↗
360 sampled nodes · 84 real cross-linksA sample of the connections. Open the map to explore every node. ↗

OPEN PROBLEMS / LASTING QUESTIONS

Choose a question
worth staying with.

Read the mathematical claim, explore known results, and follow sourced proof announcements before starting your own approach.

Browse all research problems →

01 / THE SYSTEM

Built to show its work.

Ansätze keeps the question, the search process, and the resulting evidence together—so a promising answer is the start of inspection, not the end of it.

01

A proving pipeline, not one answer

The default Ansatz CGM pipeline has a strategist propose plans, workers write lemmas and proofs, an independent verifier check each lemma in a fresh call, and a curator score what remains open.

02

Two graphs for each CGM run

Facts shows the lemmas the verifier accepted and what each one depends on. Explore shows the search itself: plans, attempts, verdicts, obstacles, and dead ends.

03

A formal Lean stage

Formalize the result in Lean 4, then compile, check, and audit the statement. A model verifier’s acceptance is never presented as a Lean certificate.

04

Continue, don’t restart

Signed-in accounts can add feedback to an existing run and continue from its workspace instead of rebuilding context.

05

Compare approaches

Run the same CGM pipeline on your own Codex, Claude Code, or API route, or try other proving engines with a common view of progress and cost.

06

Preserve useful work

Keep proofs, graphs, Lean sources, and research memory attached to the run that produced them.

02 / WORKFLOW

From question to inspectable result.

  1. 01
    Describe the problem

    Paste a statement or choose an open problem. Guests start with Ansatz CGM on Kimi K3; no key or account is needed when hosted access is available.

  2. 02
    Watch the pipeline

    Follow the strategist, workers, independent verifier, and curator as the run progresses.

  3. 03
    Inspect Facts and Explore

    Open the DAG tab to see which lemmas the verifier accepted, how they combine into the target, and which routes stalled.

  4. 04
    Check it in Lean

    The formal stage translates the proof into Lean 4. Read its status literally: compiled, verified, incomplete (sorry), wrong statement, or failed.

The Ansatz CGM pipeline adapts prompts and data contracts from the Ansatz continual-graph-memory project by FrenzyMath (Apache License 2.0). Read how a CGM run works.

03 / START HERE

Take a closer look.

Try the console in a browser-scoped guest session, sign in for durable account history, or read the main concepts first.