← Human–AI Mathematics

Conjecture search

A sustained search, by humans and AI agents, to prove or refute one hard statement, in which every result can be trusted.

On a hard question, agents produce proof attempts, reductions, numerical experiments and candidate counterexamples, over many sessions. Without structure, what was learned is lost between sessions, dead ends are explored again, and a convincing argument passes for a proof. Conjecture search gives that work one shared record, and a manuscript a mathematician can read and check.

Principles

  1. Organize the search. One target statement, a portfolio of routes and dated checkpoints, so that many agents over many sessions work as one search.
  2. Make every status trustworthy. A claim is proved or refuted only through a certification tied to the exact text examined: an independent review, or the explicit acceptance of a named person. Evidence guides the search; it never moves a status.
  3. Open the research to mathematicians. The output reads like a paper, says what is settled and what is not, and shows where a reader can help.
  4. Spend sparingly. Agent calls are the search's budget, and each one is launched for a result that needs it.

How the pieces fit together, from the life of a statement to the ways to contribute: How it works.

Projects

The KLS theorem and its methods

A manuscript on the KLS conjecture, now a theorem: a complete account of the three recent proofs, a comparison of them, and alternative mechanisms for the dimension-free Poincaré bound, produced by a sustained human–AI search. Each statement shows who checked it. Begun as a search for a proof, it has become a consolidation of the field around the theorem.

Conjecture search template

The reusable research harness behind the KLS manuscript, with no mathematics in it: a MyST manuscript, a ledger of claims and their certifications, and researcher, reviewer and writer agents. Start a new search from it.

What's next

KLS was proved while we were working on it, so the template has not yet been tested from start to finish on a question that stays open. That is our next step: run it on an open conjecture, not yet chosen, and learn whether it is pleasant for mathematicians to read, check and contribute to, whether it is efficient for what it costs, and how it should change. If you have a conjecture to propose, or would like to take part, say so in the discussions, or write to nicolas.brosse [at] ensae.fr.