Gravity is not a renormalizable QFT: black-hole entropy is not CFT entropy

Proved

GravityNonRenorm.gravity_not_renormalizable

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

black-holesquantum-gravity

Let $d\ge4$ be the spacetime dimension, $G_N>0$ Newton's constant, and let $a,b,R>0$ be the data of an arbitrary $d$ -dimensional conformal field theory on $\mathbb R_{\rm time}\times S^{d-1}$ obeying Eq. (29), with entropy-energy function $S_{\rm CFT}(E)=a\bigl(R\,(E/(bR^{d-1}))^{1/d}\bigr)^{d-1}$ (Eq. 30). Let $S_{\rm BH}(M)=\mathrm{Vol}(S^{d-2})\,r_H(M)^{d-2}/(4G_N)$ be the Bekenstein–Hawking entropy of the $d$ -dimensional Schwarzschild black hole of mass $M$ , $r_H(M)$ being the largest positive zero of $f(r)=1-\omega_{d-2}G_NM/r^{d-3}$ (Eqs. 31–32). Then it is not the case that

S_{\rm BH}(E)=\Theta\bigl(S_{\rm CFT}(E)\bigr)\qquad(E\to\infty).

This is the paper's main claim (Sec. V.1): the large-energy asymptotics of the density of states of gravity in asymptotically flat spacetime, dominated by black holes, is not that of any conformal field theory; hence gravity is not a renormalizable quantum field theory.

Formalization Note " $\sim$ " in the paper is read as $\Theta$ (two-sided bounds up to positive constants for large energies). The physical inputs (UV behaviour of renormalizable QFTs, black-hole dominance, Bekenstein–Hawking formula) are encoded in the definitions; only the resulting asymptotic incompatibility is to be proved.

Preamble

import Definitions.Def_GravityNonRenorm_Defs
import Mathlib

open GravityNonRenorm Filter Asymptotics

Formal statement

namespace GravityNonRenorm
theorem gravity_not_renormalizable (d : ℕ) (hd : 4 ≤ d) (G a b R : ℝ) (hG : 0 < G)
    (ha : 0 < a) (hb : 0 < b) (hR : 0 < R) :
    ¬ (fun M : ℝ => flatBHEntropy d G M) =Θ[atTop]
      (fun E : ℝ => cftEntropyOfEnergy d a b R E) := by sorry
end GravityNonRenorm

Source

Assaf Shomer, A pedagogical explanation for the non-renormalizability of gravity, arXiv:0709.3555v2 [hep-th] (2007), https://arxiv.org/abs/0709.3555

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement (at the explicit request of the proposal owner), not by a blind, independent auditor. The author knew the intended meaning and the source paper while writing it, so it must not be mistaken for independent testimony; reviewers should compare it against the Lean code themselves.

For every natural number $d\ge4$ and all strictly positive reals $G,a,b,R$ , it is false that the function $M\mapsto\mathrm{flatBHEntropy}(d,G,M)$ is $\Theta$ of the function $E\mapsto\mathrm{cftEntropyOfEnergy}(d,a,b,R,E)$ as the common real argument tends to $+\infty$ . Unfolded: $\mathrm{flatBHEntropy}(d,G,M)=\mathrm{sphereArea}(d-2)\,r_H^{d-2}/(4G)$ , where $r_H$ is the real supremum of $\{r>0: 1-\omega_{d-2}GM/r^{d-3}=0\}$ (value $0$ if that set is empty or unbounded), $\mathrm{sphereArea}(n)=2\pi^{(n+1)/2}/\Gamma((n+1)/2)$ , $\omega_n=16\pi/(n\,\mathrm{sphereArea}(n))$ ; and $\mathrm{cftEntropyOfEnergy}(d,a,b,R,E)=a\bigl(R\,(E/(bR^{d-1}))^{1/d}\bigr)^{d-1}$ with a real power $1/d$ . Here $f=\Theta(g)$ as $x\to\infty$ (Mathlib's IsTheta along atTop) means: there are constants $c_1,c_2>0$ and $x_0$ such that $|f(x)|\le c_1|g(x)|$ and $|g(x)|\le c_2|f(x)|$ for all $x\ge x_0$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph