Searcharxiv⌕ Search

arXiv · 2609.40324

Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

Abstract

We present Cogentic, a multi-agent harness for automated proof discovery on open research problems. While frontier language models can generate strong mathematical ideas in a single shot, single-shot generation is often insufficient for open problems that require exploring multiple competing conjectures, overcoming subtle technical obstructions, and retaining intermediate progress over a long horizon. Cogentic addresses these challenges through an iterative prove--verify loop in which an orchestrator allocates a population of independent provers across distinct proof directions, subjects their output to adversarial verification by several specialized components, and promotes confirmed intermediate results into a persistent verified ledger that later rounds build on. The harness is designed to be able to solve research-level math and theoretical computer science problems. Using Gemini as the base model, Cogentic produced novel results on five open problems across online learning, auction theory, and mechanism design. Each result was independently verified by domain experts and is developed in full in companion papers. We list these results, and new ones as they are verified, at https://sites.google.com/view/cogentic .

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang. 2026-09-30. Cogentic: Multi-Agent Orchestration for Automated Proof Discovery. https://arxiv.org/abs/2609.40324

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Generalising from Self-Produced Data: Model Training Beyond Human Constraints

Current large language models (LLMs) are constrained by human-derived training data and limited by a single level of abstraction that impedes definitive truth judgments. This paper introduces a novel framework in which AI models autonomously generate and validate new knowledge through direct interaction with their environment. Central to this approach is an unbounded, ungamable numeric reward - such as annexed disk space or follower count - that guides learning without requiring human benchmarks. AI agents iteratively generate strategies and executable code to maximize this metric, with successful outcomes forming the basis for self-retraining and incremental generalisation. To mitigate model collapse and the warm start problem, the framework emphasizes empirical validation over textual similarity and supports fine-tuning via GRPO. The system architecture employs modular agents for environment analysis, strategy generation, and code synthesis, enabling scalable experimentation. This work outlines a pathway toward self-improving AI systems capable of advancing beyond human-imposed constraints toward autonomous general intelligence.

cs.AI↗

Hierarchical Reasoning Model

Reasoning, the process of devising and executing complex goal-oriented action sequences, remains a critical challenge in AI. Current large language models (LLMs) primarily employ Chain-of-Thought (CoT) techniques, which suffer from brittle task decomposition, extensive data requirements, and high latency. Inspired by the hierarchical and multi-timescale processing in the human brain, we propose the Hierarchical Reasoning Model (HRM), a novel recurrent architecture that attains significant computational depth while maintaining both training stability and efficiency. HRM executes sequential reasoning tasks in a single forward pass without explicit supervision of the intermediate process, through two interdependent recurrent modules: a high-level module responsible for slow, abstract planning, and a low-level module handling rapid, detailed computations. With only 27 million parameters, HRM achieves exceptional performance on complex reasoning tasks using only 1000 training samples. The model operates without pre-training or CoT data, yet achieves nearly perfect performance on challenging tasks including complex Sudoku puzzles and optimal path finding in large mazes. Furthermore, HRM outperforms much larger models with significantly longer context windows on the Abstraction and Reasoning Corpus (ARC), a key benchmark for measuring artificial general intelligence capabilities. These results underscore HRM's potential as a transformative advancement toward universal computation and general-purpose reasoning systems.

cs.AI↗

A memory-based active inference model of DishBrain-like adaptive behaviour

Recent and rapid advances in artificial intelligence (AI) make it increasingly important to understand the foundations of adaptive behaviour in autonomous agents, especially for building safe and efficient systems. While artificial neural networks have dominated the development of AI, recent work has begun to explore living biological neuronal networks as an alternative substrate for computation. These systems promise remarkable data and sample efficiency and rich dynamics, and may also inspire explainable and biologically plausible models. Here, we develop an experiment-informed active inference framework to model decision-making in closed-loop agents that mirror experimental setups using biological neurons. Using a generative model whose dimensions are matched to an experiment protocol, we systematically compare three decision-making schemes within this common generative model. Under matched episode counts (i.e. total data available for learning) to the in-vitro experiment, our simulations show that agents with short memory horizons reach a level of performance close to that of mouse and human cortical cultures (DishBrain platform), whereas longer memory horizons depart from it substantially. Increasing the planning horizon, by contrast, confers no comparable benefit. Because all model parameters are explicit, we can also track the quantities in our generative model that accompany this improvement, such as the risk term and the entropy of the transition and state-action mappings. Together, these results illustrate how active inference offers a formal language for comparing decision-making schemes in similar closed-loop control environments.

cs.AI↗