---
showArticleList: false
title: Automated research
created: 2026-09-24
visible: true
status: in progress
tags: [agents, automated-research]
readability: 3
---

Where the research loop itself runs autonomously: the labs' science programs, the productized research agent, and the formal-proof engines pointed at the hardest open problems.

- [AlphaProof](alphaproof/index.md) - DeepMind's Lean reinforcement-learning solver, from IMO silver in 2024 to officially graded IMO gold via Deep Think in 2025.
- [Anthropic Claude mathematical research](anthropic-claude-math/index.md) - the Claude Code subagent loop that raised the zeta zero bound to 67.2 percent and formalized Fermat's Last Theorem in 11 days.
- [Harmonic Aristotle](harmonic-aristotle/index.md) - the free agentic theorem prover with a Lean-checked Erdős result, now aimed at software correctness, judged and contested on FormalQualBench.
- [Math Inc. Gauss](math-inc-gauss/index.md) - the autoformalization agent behind Strong PNT and the sphere-packing proof, with the comparator-audited OpenGauss harness, as of 2026-09-13.
- [OpenAI Deep Research](openai-deep-research/index.md) - the productized web-research agent, the breadth-first loop with no machine judge behind it.
- [OpenAI for Science](openai-for-science/index.md) - the lab program from FrontierMath's first open-problem solve to the disputed Navier-Stokes claim, as of 2026-09-13.
- [Pion](pion/index.md) - Andon Labs' closed research preview where persistent agents run a real business with payment tools, the Vending-Bench lineage made product.

Its members are compared on shared rows in the [Automated Research Feature Matrix](automated-research-feature-matrix/index.md).

## Changes

- 2026-09-13 - Added AlphaProof.
- 2026-09-13 - Added Anthropic Claude mathematical research.
- 2026-09-13 - Added Harmonic Aristotle.
- 2026-09-13 - Added Math Inc. Gauss.
- 2026-09-13 - Added OpenAI Deep Research.
- 2026-09-13 - Added OpenAI for Science.
- 2026-09-16 - Added Pion.