Human–AI Mathematics
Tools for mathematical research done by humans and AI agents together, so that what they produce can be trusted, read and checked by a mathematician.
AI agents can now take part in mathematical research: they attempt proofs, run experiments, read the literature and write. Their output is large, and left unstructured it works against the research: what was learned is lost, a plausible argument is mistaken for a result, and a mathematician cannot tell what is established. Mathematicians also do many kinds of work — proving or refuting a statement, understanding a field, putting what is known in order — and each calls for tools of its own. This project builds such tools, one task at a time, and tests them on real questions.
This is a proposal, not a finished method. The tools and the practice of research with AI agents change quickly, and this work will change with them. Feedback is welcome: start a discussion or open an issue on GitHub, or write to nicolas.brosse [at] ensae.fr.
Why this project
We chose the Kannan–Lovász–Simonovits conjecture as a first testbed because it was a famous, well-posed open question, one with which some of us had a passing familiarity. In October 2026 it was proved, three times: three teams, each working with frontier AI models, reached independent proofs within days of one another.
The problem was solved, and that is good news. But the effort was spent three times over, and almost none of it was shared along the way: which routes each team tried, which obstacles stopped them, which ideas they set aside. When results are judged by priority and a search leaves no common record, duplication is what one should expect, even when everyone does excellent work.
We think research with AI calls for other forms of collaboration: a shared, public record of the work, where an obstacle found once is not rediscovered and progress is pooled rather than raced. This project is our attempt at one.
Tools, by task
Conjecture search
Prove or refute one hard statement, over many sessions and many agents, with every status certified by an independent review or a named person. Its principles, the KLS manuscript it produced, and the template to start a new search.
Mathematical mapping
Map a field and consolidate what is known into an account that can be trusted and read: which results hold, how they connect, what remains open. A direction we intend to explore, not yet a project; the KLS manuscript, which became a consolidation of the field around the theorem, gives a first idea of it.