{"id":"arxiv/2609.20127","url":"https://arxiv.org/abs/2609.20127","tags":["math.DG","cs.LO"],"score":0,"title":"Retro-synthetic Riemannian geometry in Rocq I : Taylor series of a metric","domain":"math.DG","source":"arxiv","authors":["Gabriella Clemente","Hugo Herbelin","Carlos Simpson"],"reviews":0,"subject":"math.DG","summary":"We introduce a synthetic framework for doing local Riemannian geometry that is influenced by a reverse-engineering method for formalizing in Rocq. These new perspectives and techniques lead to a synthetic Taylor formula for a Riemannian metric in normal coordinates, which is the main contribution of this work.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-17","reactions":{}}