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.

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

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 single index to every SAIR Foundation challenge entered: the open problem each one states, the repository holding the method and the code, and what that method actually reached. Open science competitions in mathematics and computation, run by the Foundation for Science and AI Research.

可独立运行的数学建模工作台, 同时提供skill流程和真实多agent运行时

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.

Plectis by Will Cook: an open-source prototype for mathematical exposition and collaborative research. Eight Erdős programmes, short and long papers, Lean proofs, cross-problem mathematics and reusable infrastructure, with explicit sources, evidence and contribution credit.

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.

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.

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

A replicated experiment in adversarial, formally verified mathematical discovery

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

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

Verified prove-or-disprove harness for algebraic conjectures

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

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

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

Proof networks in the age of AI: extending Viteri & DeDeo (2022) to machine-generated mathematics

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