Scalar curvature and finite-time Ricci-flow singularities

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves that a smooth Ricci flow on a closed four-manifold extends past any finite time at which scalar curvature remains uniformly bounded. A higher-dimensional counterexample has bounded scalar curvature but unbounded full curvature at its finite maximal time, disproving the unrestricted scalar-curvature extension conjecture.

The release has no Lean statement for this family, so there is no formal statement to compare with the result described above.

What the papers state

Theorem 1.1

In A closed Ricci flow with bounded scalar curvature and finite-time curvature blowup

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

There are an integer q\ge10, a time T>0, and a smooth Ricci flow g(t), 0\le t<T, on the closed connected manifold M=\Sp^2\times\Sp^{q+1}, with smooth initial metric, such that

\sup_{M\times[0,T)}|R_{g(t)}|<\infty, \qquad \lim_{t\uparrow T}\max_M|\Rm_{g(t)}|=\infty.

In particular, T is the finite maximal existence time of this flow.

Corollary 1.2

In Bounded scalar curvature and smooth extension of four-dimensional Ricci flow

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

If a Ricci flow on a closed smooth four-manifold has finite maximal smooth existence time T, then

\limsup_{t\uparrow T}\max_{x\in M}R(g(t))(x)=+\infty.

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.

Three more possible matches

Theorem 1.1 (Smooth extension) in Bounded scalar curvature and smooth extension of four-dimensional Ricci flow.
Theorem 3.2 (Path selection) in Path selection and an elliptic inequality on degenerating Ricci-flat trees.
Theorem 2.2 (Tree inequality) in Path selection and an elliptic inequality on degenerating Ricci-flat trees.

Reported proof verification: The release has no Lean statement for this family. The papers are available to read and assess.
Papers and explanations: Three current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

A closed Ricci flow with bounded scalar curvature and finite-time curvature blowup

Undated, current edition.

Read it here PDF

We disprove the scalar-curvature extension conjecture in its unrestricted all-dimensions form. In sufficiently high dimension, we construct a Ricci flow on a closed manifold whose scalar curvature remains uniformly bounded while full curvature diverges at a finite maximal time. In one fixed sufficiently high dimension, the examples have two-sided power-law curvature blowup with arbitrarily large exponents.

Bounded scalar curvature and smooth extension of four-dimensional Ricci flow

Undated, current edition.

Read it here PDF

We prove that a smooth Ricci flow on a closed real four-manifold extends on the same manifold through every finite time at which its scalar curvature remains uniformly bounded. This resolves the scalar-curvature extension problem in dimension four.

Path selection and an elliptic inequality on degenerating Ricci-flat trees

Undated, current edition.

Read it here PDF

We prove a sequential elliptic inequality for the renormalized Einstein–Hilbert functional on a fixed finite tree of four-dimensional Ricci-flat spaces. As the joining lengths diverge and the scale-neutral weighted Ricci error M tends to zero, the functional satisfies \(E=o(M)\). The root end has decay exponent greater than one, and every joined quotient group is nontrivial. We also prove the multivariable path-selection theorem for asymptotic expansions used to obtain this estimate.

Lean statements

The release has no Lean statement for this family. Its papers remain available to read, and contributors can propose a formal statement of a result. Suggest a change

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

The release contains no Lean statement for this family, so there is no formal statement to compare with OpenAI’s description.

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Bounded scalar curvature and smooth extension of four-dimensional Ricci flow cites Path selection and an elliptic inequality on degenerating Ricci-flat trees.

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanation Suggest a source attribution Suggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Major math journal”. The page says that nothing on it is verified.
Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Identify the theorem the catalogue describes

Family 351 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

State the result in Lean

Family 351 The release has no Lean statement for this family. Open the form