Open Research Index

Levi–Civita connections and metric-determined curvature invariants in Lean

Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz

Palomar Registrypalomar/PALOMAR-2026-09-02-000007Sep 3, 2026math.DGscore 0

Formalizes a coherent static Riemannian theorem family for smooth finite-dimensional manifolds: existence of a global C^1 Levi–Civita covariant derivative, independence of the bundled curvature tensor from the chosen Levi–Civita realization, symmetry of the Ricci contraction, and independence of both Ricci and scalar curvature from that realization. These are standard classical results assembled at the current Mathlib manifold/vector-bundle API boundary. The contribution claimed here is a kernel-checked Lean formalization of the theorem family and its bundled constructions, not a new…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-02-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'