Thirty-two loops automate research today, and the row that separates them is not capability but judging: everything with a Lean kernel or an official grader behind it produces checkable artifacts, everything without one produces prose or artifacts an adversarial critic and a human must accept, and the newest columns split between a trained 8B model that is its own only judge, a five-minute keep-or-revert loss curve, a correctness-gated kernel benchmark, a campaign scoreboard of partly self-reported benchmarks, a workshop peer review the authors then withdrew from, a reviewer from a different model family, a debate-and-citation-check pipeline, an LLM-as-judge over live financial data, a bank account, a producer-critic pair, your own git worktrees, a wet lab where people still hold the pipettes, a self-hosted search stack, the open baseline the academic literature keeps citing, a grader daemon the agents are sandboxed away from, a user metric scored at every node of a code tree, logs from GPU-cluster jobs bound to the manuscript, benchmark scores over paper reproductions, a wiki with an LLM reviewer, review scores the projects publish against themselves, a held-out-data merge gate on a persistent hypothesis tree, blind reviews written to disk by a pipeline that stops before the paper, an enforced budget ledger that rejects unsupported quotes, a promotion gate that replays matched candidate and incumbent trials under a reserved false-promotion budget, and a manuscript whose every number click-traces back to the code and data that produced it. Every cell traces to its member note and that note’s fetched references.
The matrix #
How to read it #
The judging row is the deciding one, and it repeats a pattern this section tracks in software tooling: outputs are exactly as trustworthy as the verifier behind them. AlphaProof’s 2024 result and Math Inc.’s formalizations carry kernel-level guarantees; the Anthropic results add named human reviewers on top of the kernel. Aristotle’s headline claims are real where Lean checked them and contested where only the vendor graded them. OpenAI’s two entries are prose-only loops: Deep Research cites, the science program claims, and neither has a machine judge. Pion is the first proprietary column and the only one whose output is neither artifact nor prose but money: its agents run real businesses, its judge is a bank account plus the operator’s own monitoring, and its launch thread’s contradiction (the operator calling autonomous resource acquisition the most troubling capability while releasing exactly that) is recorded in its note. Agon is the first column whose judge is a critic agent on a fresh context rather than a kernel, a grader, or a full-time operator, and its paper’s own taxonomy names the failure classes that oracle cannot see, which makes it the cheapest loop to run and the least verified. OpenResearch is the first column whose loop runs on the reader’s own machine: its judge is the evidence tree it archives rather than any external oracle, which makes it the only column where the operator, the compute, and the audit trail are yours. FutureHouse Robin is the first column aimed at a wet lab rather than mathematics, code, or money: its artifacts are peer-reviewed cell-culture results, its judge is Nature’s reviewers plus the assay itself, and its paper shows both the loop’s power, a control run where Deep Research scored zero hits, and its boundary, people running every experiment. Local Deep Research is the first column that hands the reader the whole literature tier: the loop, the engines, and the models run on your machine, and its benchmark table carries its own contamination caveats, which puts it at OpenResearch’s self-hosted end of the spectrum rather than Deep Research’s product tier. GPT Researcher is the column the others get measured against: it predates the product tier, its judge is the same no-machine-oracle human read as Deep Research’s, and its distinction is being the baseline 150-plus papers cite, which makes it the least novel loop here and the most cross-checked one. Karpathy Autoresearch is the founding artifact the autoresearch family is named after: its judge is the one oracle here no vendor or model mediates, the validation curve that keeps or discards every experiment, and the scaling thread’s critiques (automated hyperparameter tuning, guided brute force) attack its ambition rather than its results. DeepAnalyze is the first column whose loop is carried by a trained model rather than a prompted harness: an 8B model plans, acts, and judges its own data analyses in one package, which makes it the cheapest loop to run, the only one with no external verifier anywhere, and the one whose self-reported benchmark claims deserve the most discount. Dexter is the first column aimed at finance: its loop plans and re-checks its own data gathering over paid statement APIs, and its judge is an LLM-as-judge plus the human, which puts its answers at Deep Research’s discount with a scratchpad audit trail as partial compensation. ARIS is the first column whose reviewer must come from a different model family: its report names the category’s shared failure mode, the plausible unsupported success, and answers it with cross-model gates rather than a kernel, which places it beside Agon as judge-by-critic while sharing DeepAnalyze’s thin independent evaluation. AutoResearchClaw is the idea-to-paper pipeline that makes citation fabrication a first-class problem: its four-layer citation check and Pivot/Refine failure loops attack the two failure classes the Lean columns never face, wrong sources and silent breakdowns, while its 54.7 percent benchmark claim remains its own. Kapso is the first column whose judge is a campaign scoreboard: its own evaluator decides every step against an objective declared in advance, and the published check comes from benchmarks, two of which (MLE-Bench and ALE-Bench) the project runs itself while the RelBench leaderboard is self-reported by design, so its claims carry DeepAnalyze’s self-report discount with the mitigating detail that the evaluator precedes the run. Sakana AI Scientist is the ancestor the idea-to-paper columns measure themselves against: its headline first passed a workshop’s peer review, and its own write-up supplies the discount (humans picked the three submissions, the paper was withdrawn by design, and none reached the authors’ own conference bar), which makes it both the founding artifact and the category’s clearest lesson in reading a milestone’s fine print. Agent Laboratory is the human-assist ancestor: its own evaluation is the family’s most quotable negative result, ten PhD reviewers scoring its papers 3.5 to 4.0 of 10 against the 5.9 accepted-NeurIPS average, while its AgentRxiv follow-up showed labs sharing papers beat isolated labs on MATH-500, which makes it the citation for both the field’s ceiling and the value of shared memory. AIDE ML is the tree-search ancestor the metric-judged columns descend from: its draft-debug-improve nodes over a user metric are the mechanism Kapso tree-searches and Weco productizes, and its MLE-Bench medal count comes from Agent Laboratory’s comparison, one column scoring another. AI-Researcher is the idea-to-paper column with the largest community and the least license: 5,802 stars against a repository with no license file, dormant since October 2025, its momentum moved into the Novix product, and its judge is the team’s own Scientist-Bench. AiScientist is the only column whose unit of work is the reproduction: its paper track drives a published paper’s full reproduction loop on PaperBench while its File-as-Bus protocol makes the workspace, not the chat, the system of record, the coordination variant the other multi-agent columns leave implicit. AutoSci is the first idea-to-paper column adapted beyond one harness: stable on Claude Code with Codex and OpenCode previews, its SciMem memory persists across projects the way Kapso’s hub does, and its reviewer is an MCP-configured model rather than an oracle. CORAL is the first column whose loop is an agent organization: islands of coding agents in isolated worktrees, a grader daemon the agents are sandboxed away from reading, and shared memory through .coral/public, which makes guarding the judge from the judged an explicit design constraint instead of a hope. NanoResearch is the idea-to-paper column that binds every number to a run: it submits its own code to local or SLURM GPU clusters and writes only from the returned logs, the self-published answer to the fabricated-results failure the citation checkers cannot see. Arbor is the first column whose judge is withheld data: gains survive only if they clear a margin on a held-out split the executors never saw, which makes it CORAL’s closest cousin with the anti-overfit gate made explicit. EvoMap AutoResearch is the idea-to-paper column that stops before the paper: its deliverable is an evidence package of runs, critic reports, and blind reviews, and its launch carried the category’s first provenance incident, a forged commit shown as Karpathy’s during a 3,278-star week. Mole is the first column with the run’s cost inside the loop’s contract: a reserve-settle ledger stops the run at the ceiling you set and verbatim-quote checks drop claims the source never said, enforcement the prose-only columns leave to the human. AutoContext is the column that makes promotion receipts the deliverable: its coach and architect output stays an immutable candidate until matched candidate/incumbent trials, a held-out lane, a field-for-field replay, and an optional audit promote it under a campaign false-promotion budget, which makes it the member whose every kept lesson arrives with the evidence that kept it. data-to-paper is the column whose judge is built into the artifact: every number, method, and dataset reference in its manuscripts is programmatically chained back through the analysis code to the data, and NEJM AI’s peer review then sampled that chain, which makes it the only member whose output carries its own audit trail, with the boundary its launch thread named, hypotheses generated from the same data the paper publishes, being the one thing chaining cannot verify. AutoKernel is the column whose oracle is a fixed benchmark on one file: the five-stage correctness harness gates every speedup the keep-or-revert loop records, which gives this domain-bound port of Karpathy’s loop the community tier’s hardest judge, while its headline numbers stay vendor-measured against PyTorch eager and torch.compile rather than CUTLASS or Ansor, the comparison its launch thread demanded and never got. The Millennium column is uniformly no: nothing here has solved one, the closest engagement is a failed-but-productive Riemann attempt and a disputed Navier-Stokes claim, and FrontierMath’s problems are explicitly built below Millennium scale.
Changes #
- 2026-09-13 - Created in the same run the Automated research category was seeded, with six columns.
- 2026-09-16 - Extended from six to seven columns with Pion (Andon Labs), appended alphabetically after OpenAI for Science, with proprietary and no-repo cells marked as such and pricing marked unverified pending the revenue-share model.
- 2026-09-25 - Updated the OpenAI for Science column for the published Lean certificates (Navier-Stokes claim now machine-checkable, acceptance and credit still pending), removed the verification preamble, linked the header row, and normalized the separator row.
- 2026-09-27 - Extended from seven to eight columns with Agon, inserted first alphabetically, with the judging prose and the failure-taxonomy boundary updated.
- 2026-09-29 - The OpenAI for Science cells moved to the documented formulation fight (Scientific American, 2026-09-21): the certificate covers Clay option C, and a September 17 three-mathematician proof shows the method cannot extend to the unforced problem.
- 2026-10-02 - Moved the AlphaProof Surface today cell for the February 2026 Gemini 3 Deep Think update, which added the first Gemini API early-access path alongside the AI Ultra rollout.
- 2026-10-05 - Extended from eight to nine columns with OpenResearch (alphaXiv), inserted alphabetically before Pion, with the intro count and the judging prose updated.
- 2026-10-06 - Extended from nine to ten columns with FutureHouse Robin, inserted alphabetically after Anthropic Claude mathematical research, with the intro count and the judging prose updated, and the OpenAI for Science Lean cell moved to the August 1 ten-proofs certificates.
- 2026-10-07 - Extended from ten to eleven columns with Local Deep Research (LearningCircuit), inserted alphabetically between Harmonic Aristotle and Math Inc. Gauss, with the intro count and the judging prose updated.
- 2026-10-07 - Extended from eleven to twelve columns with GPT Researcher (Assaf Elovic), inserted alphabetically between FutureHouse Robin and Harmonic Aristotle, with the intro count and the judging prose updated.
- 2026-10-10 - Extended from twelve to thirteen columns with DeepAnalyze (RUC DataLab), inserted alphabetically between Anthropic Claude mathematical research and FutureHouse Robin, with the intro count and the judging prose updated.
- 2026-10-10 - Extended from thirteen to fourteen columns with Karpathy Autoresearch (Andrej Karpathy), inserted alphabetically between Harmonic Aristotle and Local Deep Research, closing the founding-artifact gap in the category’s own lineage, with the intro count and the judging prose updated.
- 2026-10-10 - Extended from fourteen to fifteen columns with ARIS (wanshuiyin), inserted alphabetically between Anthropic Claude mathematical research and AutoResearchClaw, with the intro count and the judging prose updated.
- 2026-10-10 - Extended from fifteen to sixteen columns with AutoResearchClaw (aiming-lab), inserted alphabetically between ARIS and DeepAnalyze, with the intro count and the judging prose updated.
- 2026-10-10 - Extended from sixteen to seventeen columns with Dexter (Virattt), inserted alphabetically between DeepAnalyze and FutureHouse Robin, with the intro count and the judging prose updated.
- 2026-10-11 - Extended from seventeen to eighteen columns with Kapso (Leeroo), inserted alphabetically between Harmonic Aristotle and Karpathy Autoresearch, with the intro count and the judging prose updated.
- 2026-10-11 - Extended from eighteen to nineteen columns with Sakana AI Scientist (Sakana AI), appended alphabetically after Pion, with the intro count and the judging prose updated.
- 2026-10-11 - Extended from nineteen to twenty-six columns with Agent Laboratory (SamuelSchmidgall), AIDE ML (Weco AI), AI-Researcher (HKUDS), AiScientist (AweAI-Team), AutoSci (skyllwt), CORAL (Human-Agent Society), and NanoResearch (OpenRaiser), re-sorted alphabetically with the idea-to-paper and tree-search ancestors placed by title, with the intro count and the judging prose updated.
- 2026-10-12 - Extended from twenty-six to twenty-nine columns with Arbor (RUC NLPIR and collaborators), EvoMap AutoResearch (EvoMap’s Infinite Evolution Lab), and Mole (Lajos Deme), inserted alphabetically; updated the intro count and judging prose, the AlphaProof cells for the Science-published Nexus results, the OpenAI for Science cells for the lost-in-translation finding and the manuscript batch, and the Kapso surface cell for v0.7.5.
- 2026-10-13 - Corrected the pricing row label, whose fixed 2026-09-18 date contradicted the cells’ own as-of qualifiers.
- 2026-10-14 - Extended from twenty-nine to thirty columns with AutoContext (Grey Haven), inserted alphabetically between ARIS and AutoResearchClaw, with the intro count and the judging prose updated.
- 2026-10-15 - Extended from thirty to thirty-one columns with data-to-paper (Technion Kishony lab), inserted alphabetically between CORAL and DeepAnalyze, with the intro count and the judging prose updated.
- 2026-10-18 - Padded the separator row and the Lean formal verification row to the header width, the two rows the column extensions had left short.
- 2026-10-21 - Updated the ARIS column’s skill count (82 to 85) and rewrote the Karpathy Autoresearch license cells after the rotation re-verification found the README’s own MIT declaration beside the missing LICENSE file.
- 2026-10-23 - Moved the OpenResearch surface cell to v0.2.21, which widened the October Trackio integration and added the configurable SSH and Slurm storage root.
- 2026-10-23 - Extended from thirty-one to thirty-two columns with AutoKernel (RightNow AI), inserted alphabetically between AutoContext and AutoResearchClaw, with the intro count, the judging prose, and the separator and Lean row widths updated.
See also #
- AlphaProof - the officially graded DeepMind lineage
- Anthropic Claude mathematical research - the subagent-fleet loop with comparator-checked artifacts
- Harmonic Aristotle - the hosted theorem prover
- Math Inc. Gauss - the autoformalization record and audited harness
- OpenAI for Science - the lab program behind the disputed claims
References #
https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ - the AlphaProof column’s 2025 facts and the IMO grading caveat
https://www.anthropic.com/research/riemann-zeta - the Anthropic column’s zeta bound, subagent loop, and validation chain
https://aristotle.harmonic.fun/ - the Aristotle column’s surfaces, positioning, and grant program
https://math.inc/formalqualbench - the Gauss column’s audited benchmark numbers and comparator methodology
https://thenextweb.com/news/bubeck-navier-stokes-account-apology-altman - the OpenAI for Science column’s dispute facts
https://en.wikipedia.org/wiki/FrontierMath - the below-Millennium scope of the benchmark framing
https://andonlabs.com/blog/why-we-built-pion - the Pion column’s launch facts, deployment record, and the most-troubling admission
https://github.com/virattt/dexter - the Dexter column: repository, README, loop architecture, and disclaimer (as of 2026-10-10)
https://docs.gptr.dev - the GPT Researcher column: the four-stage loop, deep-research mode, and the 150-paper citation claim
| Row | Agent Laboratory | Agon | AI-Researcher | AIDE ML | AiScientist | AlphaProof | Anthropic Claude mathematical research | Arbor | ARIS | AutoContext | AutoKernel | AutoResearchClaw | AutoSci | CORAL | data-to-paper | DeepAnalyze | Dexter | EvoMap AutoResearch | FutureHouse Robin | GPT Researcher | Harmonic Aristotle | Kapso | Karpathy Autoresearch | Local Deep Research | Math Inc. Gauss | Mole | NanoResearch | OpenAI Deep Research | OpenAI for Science | OpenResearch | Pion | Sakana AI Scientist |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Operator | Samuel Schmidgall and collaborators (AMD and JHU) | AutoResearch-Factory (University of Maryland and collaborators) | HKU Data Intelligence Lab (Jiabin Tang, Lianghao Xia, Zhonghang Li, Chao Huang) | Weco AI (Zhengyao Jiang, Yuxiang Wu, and collaborators) | AweAI (paper by Guoxin Chen, Kai Jia, and coauthors including Renmin University’s Wayne Xin Zhao and Ji-Rong Wen) | Google DeepMind | Anthropic | RUC NLPIR (Renmin University) with Microsoft Research collaborators (Jiajie Jin, Guanting Dong, and coauthors) | wanshuiyin and community contributors (report by Ruofeng Yang, Yongcan Li, and Shuai Li) | Grey Haven LLC (applied AI venture studio; Jay Scambler with 2,144 of about 2,209 commits) | RightNow AI (YC-backed) | aiming-lab (the author group behind the arXiv paper, whose datasets sit under the AIMING-Lab-UNC account) | skyllwt with the paper’s 19 listed authors (Weitong Qian first) | Human-Agent Society (Ao Qu, Han Zheng, and coauthors; COLM 2026) | Technion Kishony lab (Tal Ifargan, Lukas Hafner, Maor Kern, Ori Alcalay, and Roy Kishony) | RUC DataLab (Renmin University of China) with Tsinghua University | Virattt (independent developer) | Infinite Evolution Lab at EvoMap (Yiming Ren, Xiang Liu, and coauthors; project leaders Haoyang Zhang and Junjie Wang) | FutureHouse (San Francisco nonprofit; Edison Scientific commercializes the tools) | Assaf Elovic and community contributors | Harmonic | Leeroo (YC X25) | Andrej Karpathy (independent) | LearningCircuit and community contributors | Math Inc. (DARPA expMath-supported) | lajosdeme (Lajos Deme, independent developer) | OpenRaiser (independent team; bilingual Chinese and English project) | OpenAI (product) | OpenAI (lab program) | alphaXiv | Andon Labs (YC-backed) | Sakana AI (Tokyo, with UBC and Oxford collaborators) |
| The loop produces | Research reports and code repositories from a human-supplied idea, through literature review, mle-solver experiments, and paper-solver report writing | Reviewed ideas, proposals, experiment workspaces, and paper drafts from a one-line topic | Publication-ready manuscripts and implementations from a detailed idea or a brief direction, evaluated on the team’s Scientist-Bench | ML engineering solutions: tree search over code versions that drafts, debugs, and benchmarks toward a user-defined metric | Paper reproductions from a paper bundle (PaperBench track) and metric-improving ML solutions (MLE-Bench track), coordinated through File-as-Bus workspaces | Competition-grade proofs, verified reasoning training, and, since October 2026, formal proofs of open research problems (nine Erdős problems, 44 OEIS conjectures) | New theorems and formalized proofs | Improved solutions to a stated optimization task: a coordinator’s persistent hypothesis tree of executor-coded experiments in git worktrees, where a change joins the trunk only after clearing a held-out margin | ML research runs from idea discovery through experiments to paper drafts, executed by 85 markdown skills with a persistent research wiki | Promoted context bundles (playbooks, hints, routing) plus reports, datasets, and optional trained LoRA adapters, all carried into the next run | Optimized Triton or CUDA C++ kernels with a TSV experiment log and an end-to-end speedup report, from a profiled PyTorch model | Compile-ready papers (draft, LaTeX, BibTeX) with sandbox experiment results, charts, reviews, and a citation-verification report, from a one-line idea through 23 stages | A linked research wiki plus experiments, visualizations, and papers across the full lifecycle, with SciMem memory persisting across projects | Evolved solutions to a stated task: a manager partitions coding agents into worktree islands, every committed attempt is graded, and wins are shared through persistent memory | Complete research papers from an annotated dataset, where every numeric claim is data-chained back to the code lines and data that produced it | Analyst-grade data-research reports and full data-science pipelines (preparation, analysis, modeling, visualization) from raw files | Data-backed financial research answers: planned tool runs over income statements, balance sheets, and cash-flow statements, kept in an inspectable JSONL scratchpad | Evidence packages (plans, code, run logs, metrics, critic reports, blind reviews) from discovered or supplied ideas, stopping before paper writing | Hypotheses, drug candidates, assay proposals, and data analyses around human-executed wet-lab experiments, including ripasudil for dry AMD validated in primary human RPE cells | Cited web-research reports from a plan-search-filter-write loop, with a recursive deep-research mode and LangGraph or AG2 multi-agent variants | Machine-checked proofs of stated problems | Optimized AI and data systems: each campaign searches a tree of coding-agent experiments toward a stated objective and evaluator, and harvests every trajectory into an evidence-priced knowledge hub | Kept-or-discarded nanochat training experiments, one five-minute run at a time, recorded in a results.tsv ledger | Cited research reports from agentic multi-engine search, plus an encrypted personal knowledge base built from the sources it downloads | Lean formalizations at record scale | Cited research answers and structured datasets where every claim carries a verbatim source quote and the run stops at the budget you set | Complete LaTeX papers whose numbers, tables, and figures come from experiments the pipeline submitted to local or SLURM GPU clusters and parsed from the returned logs | Cited web-research reports | Benchmark firsts and claimed solutions, published with Lean artifacts | Experiments, follow-up hypotheses, and research artifacts from autonomous loops on your own agents and compute | Real revenue-and-loss data from agents running actual businesses continuously | Fully AI-written ML workshop papers, from hypothesis through code, experiments, figures, and manuscript (v2 via progressive agentic tree search, v1 template-based) |
| Human input in the loop | A research idea, plus optional co-pilot feedback at each phase; the project measured co-pilot mode raising its review scores from 3.8 to 4.38 out of 10 | Topic and standards; built to run unattended for hours | A detailed idea description or a short research direction; the pipeline runs from there | A dataset, a goal, and a metric; the tree search runs unattended from there | A paper bundle or ML task plus GPU and time budgets; the run proceeds unattended across 24-hour horizons | 2024: manual Lean translation; 2025: none, end to end | One prompter, expert review after | A repo, an evaluator, and dev plus held-out splits; executors run unattended and main is never touched until you merge a verified gain | A research direction; the skills run unattended and pause at review gates, with the ARIS-Monitor widget flagging waits | A goal or saved scenario plus its evaluator; solve and run iterate unattended, with opt-in human judge labels through autoctx labels | A PyTorch model and a coding agent; the loop runs unattended, about 320 experiments overnight | None in full-auto; seven human-in-the-loop modes from gate-only through step-by-step co-pilot since v0.4.0 | A research topic; confirmation gates hold at destructive actions, experiment execution, and external communication | A codebase, a grader, and a task.yaml; the organization runs unattended with heartbeat-based interventions | None in autopilot from annotated data alone; or full oversight through the Copilot App, which reviews, rewinds to prior stages, and replays recorded runs | Data and a question; the trained model runs the loop unattended in a code sandbox | A financial question; the agent plans and executes with loop detection and step limits, from the CLI or WhatsApp | A research direction or idea, plus selection gates between stages; runs are stateful and can be inspected, taken over, or stopped | A disease target; humans write the protocols, run every physical experiment, and review ranked candidates before testing | A question and configuration; the loop runs unattended from there | A problem statement | An objective and an evaluator; the campaign runs unattended and its lessons carry to the next one | The program.md research-org instructions, human-edited; the agent experiments unattended overnight | A question and a strategy choice; the LangGraph agent mode picks engines and decides when to synthesize | Blueprints and scaffolding, review of key lemmas | A question and a budget ceiling in dollars or tokens; the loop runs unattended to the cap, or toolkit mode keeps your agent’s model in charge of reasoning | A research idea and a venue template; the nine stages resume from any failure | A question | Case-study curation; disputed in the math claims | A goal per direction; the loop can propose, run, and select follow-ups on its own | High-level direction only, through the Andonos managing agent | A broad topic, then humans picked the three best papers to submit; the review protocol itself was co-designed with the workshop |
| Who judges | Ten volunteer PhD reviewers scored outputs 3.5 to 4.0 of 10 on NeurIPS criteria against the 5.9 accepted-paper average the site cites, and mle-solver is scored on MLE-Bench medals; no machine judge inside the loop | Independent producer-critic agent loops on fresh contexts, plus the human for invisible failures | Scientist-Bench, the team’s own benchmark with guided and open-ended innovation tracks, plus the human reading the manuscript; no external oracle | The user’s metric at every node of the search tree, plus the human choosing the final solution; no external verifier | The target benchmark (PaperBench or MLE-Bench) plus the workspace’s system-of-record state; no external verifier inside the loop | Lean kernel plus official IMO graders | Lean comparator plus named human experts | Held-out data at the merge gate (a configurable margin), dev-split evaluation during search; the 2.5x benchmark claim is the project’s own | A reviewer model from a different family (Codex MCP by default) critiques artifacts at gates; no kernel and no benchmark | The scenario evaluator epoch scores every generation; a promotion additionally requires matched candidate/incumbent trials, a held-out lane, a replay matching the recorded comparison field-for-field, and an optional audit; no external oracle | The fixed bench.py: five-stage correctness (smoke, shape sweep, numerical stability, determinism, edge cases) must pass before timing, then measured throughput; KernelBench’s fast_p in bridge mode; no external oracle | Multi-agent debate plus a four-layer citation check (arXiv, CrossRef, DataCite, LLM) and the ARC-Bench rubric; no external oracle | An llm-review MCP model over the writing and the human at the confirmation gates; no external oracle | Your own grader daemon, isolated from the agents (a Docker sandbox since June 2026 keeps them from reading .coral/private), with optional rubric LLM judges for open-ended tasks | The manuscript’s own data-chaining, which programmatically back-traces results, methods, and data references, sampled afterwards by NEJM AI’s peer review and the human in copilot mode; no machine oracle mid-run | No external judge; the 8B model plans, acts, and self-reflects inside its own sandbox, and the human reads the report | LLM-as-judge evals logged to LangSmith, plus the human reading the answer; no machine verifier behind the data claims | Cross-model review plus independent blind reviews and critic reports written to disk; no external oracle | Nature peer review plus in vitro validation in cell culture; no machine judge inside the loop | No machine judge; the human reads the cited report, and the academic literature (150-plus papers by the docs’ count) treats it as the comparison baseline | The Lean kernel | The campaign’s own evaluator at every step, scored afterwards on external benchmarks (MLE-Bench and ALE-Bench self-run, the self-reported RelBench leaderboard, IOAI’s standardized scoring); no kernel | The measured validation loss, keep-or-revert; no model judge and no human needed mid-run | No machine judge; self-reported SimpleQA and xbench-DeepSearch community graders score the benchmarks, and the human reads the report | Lean comparator, specification-based | The budget ledger at every call, verbatim-quote checks at extraction, and contradiction detection between claims; content accuracy stays with the human | The experiment outputs themselves (the README binds every number to a run) plus per-stage model review; no external oracle | No machine judge; the human reads | Lean kernel on the published formalization; human acceptance and credit still in dispute | The evidence tree it archives (worktrees, logs, diffs, commits), reviewed by a human; no external verifier | No machine judge; the bank account plus Andon’s own monitoring | ICLR workshop peer review (double-blind, with the organizers cooperating), plus the authors’ own internal conference-track reviews; no machine verifier |
| Lean formal verification | No | No | No | No | No | Yes (2024 and the Nexus results; 2025 IMO ran in natural language) | Yes (zeta and FLT artifacts) | No | No | No | No | No | No | No | No | No | No | No | No | No | Yes | No | No | No | No | No | No | No | Yes since 2026-08-01 (the ten-proofs certificates; the Navier-Stokes ones cover Clay’s forced-blowup option, the weaker of the two formulations; October found the Navier-Stokes Lean code proves a weaker Lemma 8.6 than its written proof) | No | No | No |
| Surface today | MIT Python repository (dormant since 2025-08-20) plus AgentRxiv, the preprint server where agent labs share papers (arXiv 2503.18102) | MIT Claude Code plugin run from a separate artifacts workspace | Python repository with no license file, dormant since 2025-10-16; the commercial continuation is Novix (novix.science) | MIT Python package (aideml on PyPI, v0.2.2), the open reference build; the Weco product (weco.ai) is the commercial generalization | MIT Python repository with paper and mle workflows and benchmark integrations, dormant since 2026-07-21 | Research system; Gemini 3 Deep Think on AI Ultra plus Gemini API early access | Unreleased models; artifacts on GitHub | Apache-2.0 Python package (arbor-agent on PyPI, v0.1.4) with a replayable demo, docs, and a configurable merge margin | MIT markdown skills across Claude Code, Codex CLI, Cursor, Trae, Antigravity, GitHub Copilot CLI, OpenClaw, and DeepSeek Harness, plus the standalone ARIS-Code CLI (v0.4.28) and plugins | Apache-2.0 Python and TypeScript CLIs (PyPI autocontext 0.18.0, npm autoctx 0.19.0), a pi extension, an MCP server, and a TUI, with docs at autocontext.ai (as of 2026-10-14) | MIT Python repository (no git tags; README changelog through v1.3.0) driven by any coding agent reading program.md | MIT Python package (researchclaw CLI), OpenClaw bridge to messaging platforms, Docker executor, ARC-Bench on Hugging Face (v0.5.0) | MIT skills-and-Python platform on Claude Code (stable) with Codex and OpenCode preview branches, bilingual English and Chinese, no releases | Apache-2.0 Python package (coral CLI, v0.7.21) driving Claude Code, OpenCode, Codex, Cursor Agent, and Kiro, with docs and a blog site | MIT Python package (data-to-paper on PyPI, v1.1.22) with the Copilot App and example manuscripts; dormant since 2025-07-19 | Open weights on Hugging Face with WebUI, Docker-sandboxed WebUI v2, and CLI over vllm; a hosted API via HeyWhale key applications | TypeScript CLI on Bun (v1.1.0), WhatsApp gateway, JSONL scratchpad; OpenAI, Anthropic, Google, xAI, OpenRouter, or Ollama models | Apache-2.0 Python workflow (seven commits, no releases), bilingual English and Chinese | Open-source Apache-2.0 workflow with example trajectories; the underlying agents are commercialized by Edison Scientific | Apache-2.0 Python package, REST API stack, and Docker image (PyPI 0.16.1, GitHub release v3.7.0 of 2026-09-26) | Free web agent with login | MIT Python package (leeroo-kapso on PyPI, v0.7.10) driven through Claude Code and Codex CLIs, with cost-aware candidate selection, the Leeroopedia MCP knowledge wiki, and agent skill files | Three-file GitHub repo (prepare.py fixed, train.py agent-edited, program.md human-edited); no releases and no LICENSE file, the README itself declares MIT | MIT web app, REST API, MCP server, Docker image, and PyPI package (v1.10.7); local models (Ollama, LM Studio, llama.cpp) or cloud | OpenGauss open source; Gauss in beta | Apache-2.0 Go binary (mole plus mole-mcp) via verified script, Homebrew tap, or AUR, with an MCP server mode | MIT Python CLI (v1.0, March 2026) with Claude Code mode, a Feishu bot, and NeurIPS/ICML/arXiv templates | ChatGPT plans | Subscriptions and academic credits | MIT desktop app and orx CLI (v0.2.21), local or on your own compute | Proprietary research preview with waitlist, no repo | Open code for v1 and v2 (custom Sakana license, no standard SPDX), run on your own GPUs and API keys; both repositories last pushed 2025-12-19 |
| Pricing | Free and MIT; the site reports $2.33 (gpt-4o) to $13.10 (o1-preview) per workflow (as of 2026-10-11) | Free and MIT, no paid tier | Free to run at your own API cost; no license permits reuse and no Novix prices are published (as of 2026-10-11) | Free and MIT; costs are your own LLM API calls, with the Weco product priced separately (as of 2026-10-11) | Free and MIT; costs are your own GPUs and API calls (as of 2026-10-11) | Bundled in the Ultra subscription | Free artifacts, internal compute | Free and Apache-2.0; costs are your own model API keys and compute, no paid tier (as of 2026-10-12) | Free and MIT; costs are your own model subscriptions or API keys and compute, no paid tier (as of 2026-10-11) | Free and Apache-2.0; costs are your own model API keys or local GPU (vLLM, Ollama, MLX), no paid tier (as of 2026-10-14) | Free and MIT; costs are your own GPU and coding-agent subscription; the vendor’s enterprise optimization is a contact funnel with no published prices (as of 2026-10-23) | Free and MIT; costs are your own API keys and compute, no paid tier (as of 2026-10-11) | Free and MIT; costs are your own model access and optional Semantic Scholar API keys (as of 2026-10-11) | Free and Apache-2.0; costs are the coding-agent subscriptions the organization runs on and your compute (as of 2026-10-11) | Free and MIT; costs are your own LLM API keys, with per-run cost tracking built in (as of 2026-10-15) | Free; MIT code and open weights, costs are your own GPU, or HeyWhale-hosted API keys granted by application with no public prices (as of 2026-10-11) | Free; costs are your own API keys (OpenAI or alternatives, Financial Datasets, optional Exa), no paid tier (as of 2026-10-11) | Free and Apache-2.0; costs are your own model API keys (multi-model stages required) and compute, no paid tier (as of 2026-10-12) | Free and Apache-2.0; a paper-configured run costs about US$11 of API calls; no public Edison prices | Free and Apache-2.0; costs are your LLM tokens and any paid search-engine keys, no paid tier (as of 2026-10-11) | Free; $1,000,000 grant program | Free and MIT; costs are the required coding-agent subscriptions (Claude Code, Codex), your compute, and an optional Leeroopedia account with $20 of starter credit (as of 2026-10-11) | Free; costs are your own GPU time and model API calls, no paid tier, the README declares MIT (as of 2026-10-21) | Free and MIT; costs are your own compute and optional premium-engine API keys, no paid tier (as of 2026-10-11) | OpenGauss free; about $25 per benchmark solve | Free and Apache-2.0; costs are your own LLM and search API keys, capped by the run’s own budget flag (as of 2026-10-12) | Free and MIT; the README claims as low as $0.5 of API credit per paper with DeepSeek (as of 2026-10-11) | Plan quotas; Pro at $200/month | Program-level; GPT-5 Pro at $200/month in case studies | Free and MIT; marketplace compute at provider rates, no markup (verified 2026-10-06) | ? none published; seed tokens funded, planned revenue share | Free to run; costs are your own GPUs and LLM API keys, no paid tier (as of 2026-10-11) |
| Millennium-problem engagement | None; the targets are ML research reports, not mathematics | None claimed; mathematics is one of several domains, not the focus | None; the targets are AI research manuscripts, not mathematics | None; the targets are Kaggle-style ML engineering metrics, not mathematics | None; the targets are ML engineering and reproduction, not mathematics | None claimed; IMO as the proxy, then open Erdős and OEIS problems through Nexus | Attempted the Riemann hypothesis, failed productively (41.6 to 67.2 percent zero bound) | None; the targets are the user’s optimization tasks, not mathematics | None; the targets are ML experiments and papers, not mathematics | None; the targets are the user’s tasks and GPU-kernel studies, not mathematics | None; the targets are GPU kernel speedups, not mathematics | None; the targets are the 55 ARC-Bench topics across machine learning, physics, quantum, biology, and statistics, not mathematics | None; the targets are the user’s research projects, not mathematics | None; the paper evaluates math, algorithmic, and systems optimization tasks, not Millennium problems | None; the targets are data-analysis papers on public-health, social-network, and clinical datasets, not mathematics | None; the targets are data-analysis and reporting accuracy, not mathematics | None; the target is financial research, not mathematics | None; the targets are ML research evidence, not mathematics | None; the target is drug discovery, not mathematics | None; the targets are web-research reports, not mathematics | None public | None; the targets are ML and data systems benchmarked on MLE-Bench, ALE-Bench, RelBench, and IOAI 2026, not mathematics | None; the target is nanochat validation loss, not mathematics | None; the targets are search-and-synthesis accuracy (SimpleQA, xbench-DeepSearch), not mathematics | Strong PNT as the gateway toward the Riemann hypothesis | None; the targets are literature questions, not mathematics | None; the targets are ML papers, not mathematics | None | Navier-Stokes claimed with a Lean certificate covering the forced-blowup option, credit and formulation both disputed, and the Lean code diverges from the written proof at Lemma 8.6 | None; the targets are the user’s own research directions | None; the eval lineage is Vending-Bench, not mathematics | None; the targets are ML research papers, not mathematics |