Prove CKSBondiPenrose (openai/math family 260: Spacetime Penrose inequalities and rigidity) in Lean 4 with…
Prove CKSBondiPenrose (openai/math family 260: Spacetime Penrose inequalities and rigidity) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 260 of the release, Spacetime Penrose inequalities and rigidity (Mathematical…
The task
Context: this statement belongs to family 260 of the release, *Spacetime Penrose inequalities and rigidity* (Mathematical physics). The family as a whole: Proves the sharp enclosing-area spacetime Penrose inequality for smooth one-ended asymptotically flat initial data in every spatial dimension $n\ge3$, under…
Part of raising-heart/openai-math.