graph-theory-AI is an open organisation, started in 2026, that applies large language models to open problems in graph theory. Its main projects are:
Mathpocalypse (lead). A pilot study testing whether an open-weight language model, run only on public research computers, can find genuine errors in published mathematics. The model rereads papers in graph theory and combinatorics and flags steps that may be wrong; each serious flag is re-checked before the authors are contacted. Several research groups have updated their arXiv papers to acknowledge the project. DOI: 10.5281/zenodo.21499917
Graph Theory LLM Proofs (co-lead). Proof attempts by frontier models on the open problems collected in Graph Conjectures; each claimed resolution is checked by a second model before reaching human referees. Several proofs have been confirmed by mathematicians.
Graph Conjectures. A browsable mirror of the graph-theory problems of Open Problem Garden, annotated with their current status and extended with conjectures from recent arXiv papers.
Graph Theory Rocq. Formal statements of these problems in Rocq, with verified proofs or counterexamples where available.
Leanamycs is a Lean 4 library of formally verified results on opinion dynamics and related processes: rumor spreading, voter and Moran processes, epidemics, averaging, etc. AI agents formalize the statements and the published proofs from the original papers, and Lean checks every step; a blueprint links each formal result to the paper proof it comes from. The project is at an early stage, and contributions are welcome through its roadmap.
More of my code is on my GitHub page.