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.

Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.

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

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

ParadigmForge: a governed architecture for machine-generated mathematical theory formation (design-and-protocol paper). Extends the Bourbaki Engine from claim promotion to governed theory formation.

Audited, corrected, and verified version of the ProofNet benchmark in Lean4

Reproducible generator for Erdős problem LaTeX, metadata, status, formalization, and AI provenance

A source-linked index of open math problems solved, refuted, or settled with AI — tracking the July 2026 wave. Verification-status badges, Lean/DRAT certificates, priority caveats.