发表机构
Université Paris Cité, CNRS, IRIF; Université Paris Cité, INRIA, IRIF; Université Côte d’azur, CNRS, LJAD（巴黎西岱大学，法国国家科学研究中心，IRIF; 巴黎西岱大学，法国国家信息与自动化研究所，IRIF; 蔚蓝海岸大学，法国国家科学研究中心，LJAD）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一个受逆向工程启发的合成框架，用于在 Rocq 中形式化局部黎曼几何，并导出正规坐标下度量的合成泰勒公式。
AI 中文摘要
我们引入了一个用于局部黎曼几何的合成框架，该框架受到一种在 Rocq 中形式化的逆向工程方法的影响。这些新视角和技术导出了正规坐标下黎曼度量的合成泰勒公式，这是本工作的主要贡献。
英文摘要
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.
