openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Frontier

Frontier API →

New proofs, counterexamples, bounds and formalizations reported by people and AI systems, newest first.

Reported developments, attributed to their sources. Inclusion is not an OpenMath assessment; evidence slots show what each source reports. Updated Oct 13, 2026.

February 2026 12

New proofTheoretical computer scienceGemini case 7.5

Entropy, low-rank and Chamfer streaming

Case 7.5 in the Gemini Deep Think research report (multiple algorithmic bounds).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 7.4

Streaming submodular maximization

Case 7.4 in the Gemini Deep Think research report (analysis with hypothesis correction).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 7.3

Robust coresets

Case 7.3 in the Gemini Deep Think research report (construction bound).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 7.2

Local-search query complexity

Case 7.2 in the Gemini Deep Think research report (bounds).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 7.1

Biclique partitions

Case 7.1 in the Gemini Deep Think research report (bounds).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 6.1

Cosmic-string spectral integrals

Case 6.1 in the Gemini Deep Think research report (closed form derivation).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 5.1

Search versus decision in S₂ᴾ

Case 5.1 in the Gemini Deep Think research report (algorithmic research).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 4.3

Regular bipartite perfect matchings

Case 4.3 in the Gemini Deep Think research report (bounds with prior literature corrections).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 4.2

Steiner-tree graph embeddings

Case 4.2 in the Gemini Deep Think research report (conjecture specific proof).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 4.1

Max-Cut geometry

Case 4.1 in the Gemini Deep Think research report (supporting lemma).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofTheoretical computer scienceGemini case 3.2

SNARG proof bug

Case 3.2 in the Gemini Deep Think research report (proof error detection).

Gemini Deep Think research version · Google DeepMind
LFCR
New proofCombinatoricsErdős #1089

Erdős problem #1089

Full solution found. Contribution type: AI alongside literature.

Aletheia
LFCR

January 2026 15

New proofCombinatoricsErdős #1051

Erdős problem #1051

Full solution (Lean). Contribution type: AI standalone.

Aletheia
LFCR
New proofCombinatoricsErdős #1148

Erdős problem #1148

Full solution. Contribution type: AI collaborating with humans.

Gemini 3 Pro · Gemini 3.1 Pro · GPT-5.2 Pro · GPT-5.2 Thinking · GPT-5.4 Pro · Ingo Althöfer · Przemek Chojecki · Wouter van Doorn
LFCR
New proofCombinatoricsErdős #543

Erdős problem #543

Full solution. Contribution type: AI alongside literature.

GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #1047

Erdős problem #1047

New proof found (Lean). Contribution type: AI building on literature.

Aristotle
LFCR
New proofCombinatoricsErdős #1007

Erdős problem #1007

New proof found (Lean). Contribution type: AI building on literature.

Aristotle
LFCR
New proofCombinatoricsErdős #281

Erdős problem #281

Full solution. Contribution type: AI alongside literature.

GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #224

Erdős problem #224

New proof found (Lean). Contribution type: AI building on literature.

Codex · GPT-5.2 Thinking
LFCR
New proofCombinatoricsErdős #659

Erdős problem #659

Full solution. Contribution type: AI collaborating with humans.

Gemini 3 · Benjamin Grayzel
LFCR
New proofCombinatoricsErdős #401

Erdős problem #401

Full solution (Lean); solution to variant problem. Contribution type: AI collaborating with humans.

Aristotle · GPT-5.2 Pro · Boris Alexeev, Kevin Barreto, Liam Price +1
LFCR
New proofCombinatoricsErdős #397

Erdős problem #397

Full solution (Lean). Contribution type: AI alongside literature.

Aristotle · GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #205

Erdős problem #205

Full solution (Lean). Contribution type: AI standalone.

Aristotle · GPT-5.2 Thinking
LFCR
New proofCombinatoricsErdős #729

Erdős problem #729

Full solution (Lean). Contribution type: AI building on literature.

Aristotle · GPT-5.2 Pro
LFCR
New proofCombinatoricsErdős #728

Erdős problem #728

Full solution (Lean). Contribution type: AI alongside literature.

Aristotle · GPT-5.2 Pro
LFCR

October 2025 1

New proofCombinatoricsErdős #347

Erdős problem #347

Full solution (Lean). Contribution type: AI collaborating with humans.

Aristotle · Claude Opus · Codex · GPT · Enrique Barschkis, Wouter van Doorn, jbbaehr22 +2
LFCR

Date not recorded 1