ai-for-math

Formal verification for AI: a Lean 4 + Dafny proof checker that catches fake AI proofs (reward hacking), and verified recursive self-improvement (RSI) for coding agents. AI for math, physics and software engineering.

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.

Computational number theory and Lean 4 formalization around the Riemann zeta function: a kernel-checked RH to height 100, checked proofs, rigorous numerics and negative controls. Makes no claim to have proved RH.

Mathematical results from the Argus research agent: verified improvements across all 373 families of OpenAI's openai/math collection, 84 open-problem result packages, Lean 4 certificates.

Papers, proofs and research records for eight Erdős problems, including what is established and what remains open.

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

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.

[NeurIPS 2026] Audited, Corrected, and Verified Version of The ProofNet Benchmark in Lean4

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.

MathVet: independent, pre-referee fidelity reviews of AI-generated Lean formalizations. First review: openai/math (235 families). Does the Lean statement say what the paper claims?

AI 赋能统计研究：原理、工作流与应用实践 — 面向统计背景 AI 初学者的 21 章开源技术手册 | AI for Statistical Research: Principles, Workflows, and Applications

Reconstructed and certified proofs of the KLS conjecture, and the record of the search around it.

Independent exact certification of machine-generated mathematics — exact arithmetic, no code shared with the claimant, refusal as a verdict.

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.

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

Five volumes, 4,020 pages: the meta-reasoning kernel of the Grothendieckian Programme. Reasoning native to a topos: a context is a site, evidence is a sheaf over it, and a conclusion is a global section that exists only where the local evidence glues. Open access, DOI 10.5281/zenodo.23538544.

Five volumes, 1,309 pages on the Hodge Conjecture: algebraicity as a descent datum along a definable prism, twelve axioms, an unconditional equivalence of five formulations, nine obstructions of which two are live. The Hodge conjecture remains open. Open access, DOI 10.5281/zenodo.23597954.

Content of Math 2.0, a versioned knowledge graph of mathematics. Each node has a permanent tag, sources and a computed status. Lean 4 and Mathlib check the formal proofs.

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

Five volumes, 1,666 pages on the abc conjecture: a global substrate over which Spec Z acquires a base, strain, the Theta-dilation, an unconditional trace-invariance theorem, Theorems A and B conditional on 98 named obligations, and abctk. The abc conjecture remains open. DOI 10.5281/zenodo.23610034.