Automatic Certified Differentiation in Lean

DOI10.48550/ARXIV.2610.36396MaRDI QIDQ7408761arXivFDO

Authors Ramy Shahin

Publication date 26 October 2026

Published in arXiv

Tldr We present an automatic certified differentiation method that leverages Lean proof assistant for correctness and efficiency. Our method indexes derivative theorems by their domains to ensure correctness and reduces search space through efficient indexing.

Full work available at URL https://doi.org/10.48550/ARXIV.2610.36396

arXiv classification

cs.MScs.SC

This page was built for publication: Automatic Certified Differentiation in Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7408761)