Hamiltonian decomposition of Z_m^3 Cayley digraphs for all m > 2 — a complete solution to Knuth's "Claude's Cycles," found by LLM agents under a structured exploration prompt. Constructions, proofs, Lean formalization, and a verification suite.

AI-generated solutions to two research-level math problems from the First Proof community experiment: a Yang-Mills gauge-fixing heat-flow estimate on the 2-torus, and sharp fatness of geodesic triangles in sparse random graphs. Produced autonomously in Claude Code, offered for human validation.

Retrieval-grounded reviewer-memory tool over closed-PR review history of leanprover-community/mathlib4. Indexes ~158k past reviewer comments across ~35k closed PRs to flag concerns past reviewers have raised before.

Weighted Erdős–Szekeres (Erdős #1026) in Lean 4 / Mathlib — human-scale proof plus a referee report, failure atlas, and extracted benchmarks for AI theorem-proving

AI powered conjecture exploration engine. Generates candidate mathematical hypotheses via LLM, auto-formalizes them in Lean 4, and logs every experiment in a reproducible, snapshot-based research environment. Built on ProofX infrastructure.

Benchmark for rare-event evaluation in AI for Math using knot polynomial coefficient spaces.