Formal-Informal Mathematical Alignment through and beyond Human Annotations

DOI10.1145/3799682.3839951MaRDI QIDQ7401841arXivFDO

Authors Noah Gießing, Hamid Rahkooy, André Greiner-Petter, Moritz Schubotz, Ankit Satpute

Publication date 22 October 2026

Published in arXiv

Tldr We construct a dataset of alignments between informal statements from the Stacks Project and their formalizations in Lean's \texttt{mathlib} using expert annotations, facilitating exploration and reuse of formalized mathematical knowledge via MaRDI.

Full work available at URL https://doi.org/10.1145/3799682.3839951

arXiv classification

cs.IR

Cites work

• A survey of languages for formalizing mathematics
• Aspect-Aware Content-Based Recommendations for Mathematical Research Papers
• Formalising the Proj construction in Lean
• Hammering towards QED
• Stacks Project
• The Lean mathematical library
• The Lean mathematical library

This page was built for publication: Formal-Informal Mathematical Alignment through and beyond Human Annotations

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