About this collection

This is a collection of fully autonomous agentic research in mathematics, mathematical physics and theoretical computer science: the results of my experiments with large language models working as autonomous research agents on open problems.

How the results were produced

AI agents chose the approaches and produced the research, proofs, computations, Lean formalizations and manuscripts. I decide what to publish and am responsible for it. The results have not been externally peer reviewed. Each manuscript states its own contribution history, and the authorship record gives the full account.

GPT 6 Astra by OpenAI, in ChatGPT and Codex
GPT 6.1 Sol by OpenAI, in Codex
Opus 5.5 by Anthropic, in Claude Code

Each manuscript states how these models were used for it.

How the proofs are checked

Every result links its Lean 4 formalization. 7 result families use the shared library in lean/, where Comparator checks selected theorems against separate Challenge statements. The other 47 results have standalone packages with their own toolchains and instructions.

A formal check covers only the statement that was checked. It does not establish novelty or historical priority. Each result page states its formal scope and limits, and UNFINISHED.md lists the remaining formalization gaps. The verification guide gives the reproduction commands.

Selected results

I mark 11 results as selected: the ones I consider the strongest in the collection. This is my own selection, not an external assessment, and the same scope statements and limits apply. Results with earlier or overlapping work recorded in the priority and novelty record are not selected, with one exception explained there and in the README. Exchanges with researchers are listed under research correspondence; they do not imply verification or endorsement.

Citation and license

Cite an individual result with the citation file linked from its page. Cite the collection with CITATION.cff or CITATION.bib. The repository license applies except where NOTICE identifies third-party material.

Colophon

The pages are generated from catalogue.json and CONTENTS.md by site/build.py. Text is set in the reader’s own serif, Charter where it is available, with small capitals for labels. The site loads no web fonts, analytics, cookies, trackers or other external resources. A machine-readable result index and a sitemap list every result.