Math / AI

openai/math repo

5 commits · last commit 2026-10-12

Mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model on open research problems.

• 719 manuscripts in 372 families, classified by mathematical discipline.
• Some results come with Lean formalizations; the rest are not yet verified and may contain issues.
• Includes abridged reasoning summaries for selected results.

#003

The quasi-Riemann hypothesis preprint: every Dirichlet $L$-function, including $\zeta(s)$, is zero-free in $\mathrm{Re}(s)>7/8$. The same half-plane is zero-free for every finite-order Hecke $L$-function over $\mathbb{Q}(\sqrt{-3})$.

• Companion preprint 11/12 proof: a proof of the zero-free half-plane $\mathrm{Re}(s)>11/12$.
• Companion preprint Landau–Siegel: uniform exclusion of Landau–Siegel zeros.

#109

Integer multiplication below $n\log n$ preprint: deterministic $O(n(\log n)^{1-\kappa})$ time with $\kappa=2^{-182}$ on a multitape Turing machine, disproving the Schönhage–Strassen $n\log n$ optimality conjecture in that model.

• CrocSwap/integer-mult-bounds repo: a community effort to optimize the construction and push $\kappa$ higher. It is conditional on the #109 framework and is not an official OpenAI release.
• Status (updated 2026-10-26):
  • Past selected: #1094, $\kappa\approx 0.00167$; #4359, $\kappa=0.0023$; #4470, $\kappa=0.00302015$; #4610, $\kappa=0.0030217758$; #5413, $\kappa=0.003027288235$ (maintainer-reviewed).
  • Reviewed checkpoint: #4416, $\kappa=0.00268647$ (merged, maintainer-reviewed, not selected).
  • Selected: #5599, $\kappa=0.00310045$ (maintainer-reviewed, not a complete Lean multiplication theorem).

Repositories accompanying DeepMind's work on mathematical and algorithmic discovery.

google-deepmind/formal-conjectures repo

2,931 commits · last commit 2026-10-21

Lean formalizations of the statements of open conjectures, useful as a benchmark for automated theorem provers.

google-deepmind/alphaevolve_repository_of_problems repo

61 commits · last commit 2026-07-11

67 mathematical problems with prompts, verification code and evolved programs from Mathematical exploration and discovery at scale.

google-deepmind/alphaevolve_results repo

39 commits · last commit 2026-01-05

Colab notebook with AlphaEvolve's mathematical discoveries and the code verifying them.

google-deepmind/funsearch repo

14 commits · last commit 2024-02-05

Functions and sets discovered by FunSearch (cap sets, admissible sets, bin packing, and more) and the search pipeline.

google-deepmind/alphadev repo

3 commits · last commit 2023-06-20

Pseudocode of the AlphaDev agent and the discovered assembly programs for small sorting algorithms.

anthropics/formal-math repo

31 commits · last commit 2026-10-06

Machine-checked Lean 4 formalizations published by Anthropic. Each project is a self-contained Lake project following the Palomar submission layout.

zeta23

More than two thirds of the zeros of the Riemann zeta function are simple and on the critical line.

3sum-apsp

The first polynomial improvements over the textbook $O(n^2)$ 3SUM and $O(n^3)$ APSP algorithms on a word RAM, followed by a simplified proof and smaller exponents.

• Alman and Vassilevska Williams: $O(n^{1.9992})$ for 3SUM and $O(n^{2.99942})$ for APSP, via triangles in sparse lopsided graphs. arXiv:2610.06783
• Karingula and Lovett: a simplified proof of the polynomial improvements, with weaker exponents. arXiv:2610.15663
• Majdoddin: improved exponents $n^{1.99450+o(1)}$ for 3SUM and $n^{2.99450+o(1)}$ for APSP. arXiv:2610.17420

deepseek-ai/DeepSeek-Prover-V2 repo

2 commits · last commit 2025-07-18

Open-source language model for formal theorem proving in Lean 4, trained with reinforcement learning on subgoal decomposition.

• Cold-start data comes from recursive proof search: DeepSeek-V3 decomposes a theorem into subgoals and a 7B prover solves each one.
• DeepSeek-Prover-V2-671B reaches an 88.9% pass ratio on MiniF2F-test and solves 49 of 658 PutnamBench problems.