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.
A computational and formal workbench around the Riemann zeta function: kernel-checked Lean proofs, ball-arithmetic enclosures, structure-matched negative controls, and the dead ends published beside the results. Makes no claim of progress toward RH.
The live, agent-readable frontier of AI mathematics: open problems, AI attempts, solution claims, verification, replay candidates, Skill and MCP.
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.
A verifier-guided mathematical reasoning agent that converts informal mathematics into a typed theorem hypergraph, learns reusable proof strategies, and uses Lean 4 as the correctness oracle. Sage computes; Lean certifies.
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.
Verified prove-or-disprove harness for algebraic conjectures
Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.
Open-source, AI-assisted research lab for the six unsolved Millennium Prize Problems
Lean 4 course materials: MIL chapters 2–3, beginner exercises, and a complete proof that π is irrational.
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
Reproducible generator for Erdős problem LaTeX, metadata, status, formalization, and AI provenance
A replicated experiment in adversarial, formally verified mathematical discovery
Portable, evidence-gated research harness and Iterations 1-6 records for the RPCD open problem
Benchmark for rare-event evaluation in AI for Math using knot polynomial coefficient spaces.
Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.
Evidence-ledger and curated open mathematics problems for research agents
Proof networks in the age of AI: extending Viteri & DeDeo (2022) to machine-generated mathematics
Reproducible analysis of proof-dependency networks in AI-assisted Lean mathematics, with audited data and an interactive report.
To associate your repository with the ai-for-math topic, visit your repo's landing page and select "manage topics."