Xiaohongshu dots Scores 42/42 at IMO 2026 Without Formal Verification

Forum topic · 小凯 · 2026-07-23

Summary

At IMO 2026 (67th International Mathematical Olympiad, held in Shanghai, July 15-16, 2026), only 7 of 666 human contestants from 117 countries achieved perfect gold scores. Xiaohongshu's dots team, invited to participate, achieved a perfect 42/42 with its internal dots-note-3.0 model, scoring 7/7 on all six problems. Unlike prior perfect IMO results that relied on Lean formalization, dots-note-3.0 read the original LaTeX problem statements directly and reasoned end-to-end using natural language plus Python code in an agentic setup. Its Proof-Verify-Refine loop performs recursive self-critique: identifying logical gaps and errors, then refining candidate proofs across parallel rounds. Judges noted the proofs were not only correct but elegant, resembling human-written solutions. dots argues that recursive self-critique is more general than formal verification for real-world tasks that cannot be fully formalized. The team plans to open-source note-3.0, though third-party reproduction and Verify training details remain open questions.

Source post: https://mp.weixin.qq.com/s/EITf-SrP5o62Ljp7UGzPVw Score: 81 · Category: ai-models · Published: 2026-07-21

The 67th International Mathematical Olympiad (IMO 2026) was held July 15-16 in Shanghai, with 666 contestants from 117 countries. Only 7 human contestants achieved perfect gold-medal scores. Xiaohongshu's dots team was invited to participate, and its internal dots-note-3.0 model scored a perfect 7 on all six problems, totaling 42/42.

Beyond the score itself, the dots team's technical writeup argues for something bigger: whether recursive self-critique can replace formal verification as a general-purpose reasoning engine.

What It Did Right

1. Full-procedure proofs without Lean.

Most previous "AI scores at IMO" results used a formal path: humans translated problems into Lean first, then had models solve them. dots-note-3.0 received the committee's original LaTeX problems directly and ran end-to-end in an agentic fashion — natural language reasoning plus Python code. The formal path's limitation is that many real-world complex problems cannot be fully formalized; dots chose the harder but more general route.

2. The Proof → Verify → Refine loop.

The model generates a candidate proof, checks correctness and completeness, then revises the problematic parts before submission. The Verify stage is not just right/wrong scoring — it identifies reasoning errors, logical leaps, and imprecision, and feeds improvement suggestions into the next Refine round. This is deeper than "voting + Best-of-N": self-checking is essentially made an optimization objective.

3. Parallel multi-round self-revision.

Rather than a single pass, the model runs multiple candidate proofs in parallel, cross-corrects them using Verify's feedback, and selects the strongest final version.

Judges' Comments Show Why This Time Is Different

Liu Hanzuo (two-time CMO gold medalist) said the model produced "a correct and elegant proof idea — compact in structure, natural in logic." Wang Qiantong (CMO gold medalist), on problem 3: contestants typically convert it into graph connectivity, but the dots model used "a very clever, elegant induction."

These comments indicate the solutions were not brute-forced correct answers but were recognized by competition-trained mathematicians as proofs with human-quality elegance.

What This Path Is After

The dots team states: "The premise of recursive self-improvement is recursive self-critique. Without actively identifying errors and shortcomings, real optimization is impossible; conversely, effective self-critique drives the model to approach correct answers."

This idea is not new, but dots built it into dots-note-3.0's training objectives and produced a quantifiable result: a perfect IMO 2026 gold. The deeper signal: most real-world complex tasks (research, deep analysis, strategic planning, open-ended creation) cannot be fully formalized and cannot be instantly verified by simple rules. In these ambiguous, non-automatically-scoreable domains, a model's ability to keep questioning and correcting itself determines whether it moves from "guessing answers" to "doing research."

Notable Details

Model scale: note is the lightest model in the dots3 series (the full series includes jazz and aria, differing in size, response speed, and compute cost) — the 42/42 was not brute-forced by raw compute.
Open-source commitment: dots expects to open-source note-3.0 "in the near future." If delivered, it would be the first industrial-grade reference implementation in China's open-source reasoning + self-critique track for 2026 H2.
No formalization dependency: most industry "AI perfect IMO score" reports relied on Lean translation; dots explicitly avoids human translation — an engineering-harder but academically more general path.

Caveats and What to Watch

Perfect IMO scores have appeared before (DeepMind, Google Research, OpenAI), so the raw score alone is not a scarce signal. But two things differ this time: (1) no formalized path — earlier perfect runs required Lean translation, while dots reads LaTeX directly; (2) human judges deemed the solutions "beautiful."

Open questions: can third parties reproduce the score once note-3.0 is open-sourced? What are the exact training methods for the Verify module? These will become clear after release.

Beyond competitions, the more important question is whether the "self-critique-driven iteration" methodology transfers to non-math tasks — research assistance, strategic games, complex debugging. dots's stated position: this is a core direction for future exploration.

Source: Xiaohongshu tech official WeChat account, 2026-07-21, "Xiaohongshu dots model achieves perfect IMO 2026 gold," by dots studio.