# Formalization of Optimality Conditions for Smooth Constrained Optimization Problems

arXiv: https://arxiv.org/abs/2503.18821 · HTML: https://mlsanity.com/paper/2503.18821/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Mar 2025.

## Built on by (most cited first, 1 of 1)

- [Where Paths Collide: A Comprehensive Survey of Classic and Learning-Based Multi-Agent Pathfinding](https://mlsanity.com/paper/2505.19219/) (2025)

## Abstract (arXiv)

Optimality conditions are central to analysis of optimization problems, characterizing necessary criteria for local minima. Formalizing the optimality conditions within the type-theory-based proof assistant Lean4 provides a precise, robust, and reusable framework essential for rigorous verification in optimization theory. In this paper, we introduce a formalization of the first-order optimality conditions (also known as the Karush-Kuhn-Tucker (KKT) conditions) for smooth constrained optimization problems by beginning with concepts such as the Lagrangian function and constraint qualifications. The geometric optimality conditions are then formalized, offering insights into local minima through tangent cones. We also establish the critical equivalence between the tangent cone and linearized feasible directions under appropriate constraint qualifications. Building on these key elements, the formalization concludes the KKT conditions through the proof of the Farkas lemma. Additionally, this study provides a formalization of the dual problem and the weak duality property.