AI Proof WatchKeep up with AI contributions

Faster-than-power-law decay of order parameter correlations in the two-dimensional RP2 model: a rigorous result by vibe-proving

Masaki Oshikawa

In the two-dimensional nearest-neighbor RP² and RP³ projective spin models, the quadrupolar two-point correlation is bounded by Cβ exp[−cβ(log(2+r))²] for every finite coupling bound β. The positive constants are uniform over finite square-lattice subgraphs, signed couplings |bₑ|≤β and observation sites; r is their lattice ℓ∞ distance. The spherical observables are (nₓ·nᵧ)²−1/3 and (qₓ·qᵧ)²−1/4.

Sources for this record

What was already known

Projective spins identify opposite directions and permit Z₂ vortices. Numerical and heuristic work left possible algebraic quadrupolar correlations disputed. The proof adapts the released fourth-order response and annular methods for O(n) spins to squared interactions and projective observables.

AI involvement AI-autonomous

Masaki Oshikawa says he asked for the result without supplying the scientific or mathematical insight behind its proof. GPT-6 Astra generated the proof and formalization; Claude reviewed and suggested changes. Oshikawa chose the models and generalizations, supplied physical context and prepared the release.

Importance Notable

Rules out a power-law tail of this order parameter at every finite temperature within the stated models.

Limitations

The bound is slower than exponential and does not rule out every phase transition or prove vortex unbinding. The selected checks cover finite-volume quadrupolar statements, not the paper’s heuristic renormalization-group discussion or every local-limit claim. Oshikawa says he is not qualified to verify the mathematical proof; the written exposition may differ from the formal proof.

Technical verification Formal (Lean)

The exact challenge defines normalized spherical Gibbs measures, squared interactions and the two centered observables. Palomar reports successful protected comparison and Lean, NanoDa and con-ron checks of both log-square bounds, without an assumed decay or annular-response certificate.

Formal checking

Protected comparison and independent kernel checks of ProjectiveDecay.rp2_log_square and rp3_log_square under standard axioms

Checker
Palomar: Lean, NanoDa and con-ron
Scope
In the two-dimensional nearest-neighbor RP² and RP³ projective spin models, the quadrupolar two-point correlation is bounded by Cβ exp[−cβ(log(2+r))²] for every finite coupling bound β. The positive constants are uniform over finite square-lattice subgraphs, signed couplings |bₑ|≤β and observation sites; r is their lattice ℓ∞ distance. The spherical observables are (nₓ·nᵧ)²−1/3 and (qₓ·qᵧ)²−1/4.
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Few

Few is the default when evidence for a higher level is insufficient. Oshikawa explicitly says he cannot verify the mathematical proof in a short period and credits the proof exposition to AI. His physical interpretation does not establish a human account of the central mathematical mechanism.

Correction and publication history