MathLoop
How it works Verify a Lean proof Donate

Open problems need time to think.

Help AI work on open math problems.

Your contribution helps pay for long, careful AI research. MathLoop chooses the problems, runs the work, and shares what we learn.

No account to create. No subscription. Just one contribution.

Proofs and research traces

Check a Lean proof—and share the trail behind it.

Send us a public Lean project. We rebuild it in a clean environment and publish what we checked. When a proof comes from a public frontier-model trace, the prompt, attempts, and repairs can sit beside the source so others can learn from the data.

Submit a Lean proof for review

We’re setting up the review checkout.

  1. 1
    Share the project and its trail

    Send the repository and exact commit. If there is a public model trace, include that too.

  2. 2
    We run a clean build

    We record the Lean version, dependencies, result, and fingerprints.

  3. 3
    Publish the checked work

    Passing builds get a public verification page, with the trace linked when one is available.

How MathLoop learns

How we work through a problem

We keep failed ideas, counterexamples, and criticism visible. That makes the final result easier to trust and easier for others to check.

The big idea

Learn from the whole trail, then write a better prompt.

We study public frontier model research traces—the full trail of the original prompt, failed approaches, counterexamples, criticism, proof drafts, and repairs.

We use what we learn to shape the next prompt. The problem stays the same, and we spell out what a real answer needs to show before we begin.

Explore the published Erdős materials ↗ Read the prompt that inspired the method ↗
  1. 01
    Read the trail

    See what was tried, where it broke, and which ideas survived criticism.

  2. 02
    Pull out the lessons

    Keep the useful moves, failed routes, edge cases, and checks.

  3. 03
    Write a sharper prompt

    Give the next problem its own finish line, traps, and review plan.

  4. 04
    Run the loop again

    Try, challenge, repair, and report the new attempt.

The seven-step playbook

A careful attempt, from problem choice to an honest report.

The prompt changes with the problem. The discipline stays the same.

  1. Loading the research steps…

The work / 03

Problems we are following

Each problem shows what was claimed, what we checked, and what still needs review.

Loading the problem files…