An introduction to mathematical formalization based on lean

DOI10.12286/JSSX.J2024-1273MaRDI QIDQ6916482zbMATH OpenFDO

Authors Chenyi Li, Zaiwen Wen

Publication date 15 October 2025

Published in Mathematica Numerica Sinica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.12286/JSSX.J2024-1273

zbMATH Keywords

computational mathematicsformalizationoptimization

Mathematics Subject Classification ID

Numerical optimization and variational techniques (65K10) Formalization of mathematics in connection with theorem provers (68V20) Nonconvex programming, global optimization (90C26)

Cites work

• An elementary formal proof of the group law on Weierstrass elliptic curves in any characteristic
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality
• Isabelle/HOL. A proof assistant for higher-order logic
• The directed Van Kampen theorem in Lean
• The Lean theorem prover (system description)
• Towards solid abelian groups: a formal proof of Nöbeling's theorem

This page was built for publication: An introduction to mathematical formalization based on lean

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