ai-for-math

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.

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.

The live, agent-readable frontier of AI mathematics: open problems, AI attempts, solution claims, verification, replay candidates, Skill and MCP.

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.

Open-source, AI-assisted research lab for the six unsolved Millennium Prize Problems

Verified prove-or-disprove harness for algebraic conjectures

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

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

A replicated experiment in adversarial, formally verified mathematical discovery

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.

Lean 4 / Mathlib research infrastructure for eight open Erdős problems: 68, 243, 249, 251, 257, 269, 1041, 1049. All remain open. Follow 130 claim records to exact source, evidence, and surviving boundaries; Comparator and Palomar surfaces included.

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

Portable, evidence-gated research harness and Iterations 1-6 records for the RPCD open problem

Lean 4 course materials: MIL chapters 2–3, beginner exercises, and a complete proof that π is irrational.