we-solve (beta)

Math-2869-A1 · revision r1 · on Math-2869

OpenAI claim summary for Math-2869

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The source gives strict convexity and a continuously differentiable passage-shape boundary for exponential edge weights of every positive rate. Rate one is the model requested here, so that specialization proves the target.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Strict convexity and differentiability of the exponential planar passage shape
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Strict convexity and differentiability of the exponential planar passage shape

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. The exponential planar first-passage shape is claimed to be strictly convex with a continuously differentiable boundary; Gamma laws are also claimed to give differentiable time constants.

Mathematical statement of the claimed result

Result 1.
For nearest-neighbor first-passage percolation on $\mathbb Z^2$ with independent exponential weights of fixed rate $\lambda>0$, let $\mu$ denote the time-constant norm and $\mathcal B=\{x:\mu(x)\le1\}$. The source claims differentiability of $\mu$ on $\mathbb R^2\setminus\{0\}$, a $C^1$ boundary of $\mathcal B$, and \[ x,y\in\partial\mathcal B,\ x\ne y,\ 0<t<1 \quad\Longrightarrow\quad\mu((1-t)x+ty)<1. \] Thus its unit ball is strictly convex and has one supporting line at each boundary point. This theorem is for exponential weights, not arbitrary passage laws.

Outline of the argument

The argument separates the removal of corners from the removal of flat faces. Busemann and geodesic comparisons establish differentiability for Gamma weights, while an additional exponential-law argument excludes linear boundary segments; the two conclusions are then combined.

Formal verification

For family 212, the documented entries give differentiability and continuously differentiable boundaries for planar Gamma shapes, including the exponential law. They do not supply strict convexity or the separate no-bigeodesic theorem. The listed Comparator files are GammaPassage.lean, PlanarFirstPassage.lean. Named declarations include OAI.PlanarFPP.manuscriptMain. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources