Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalization of Optimality Conditions for Smooth Constrained Optimization Problems

Chenyi Li, Shengyang Xu, Chumin Sun, Li Zhou, Zaiwen Wen

TL;DR

This work presents a Lean4 formalization of first-order optimality conditions for smooth constrained optimization, grounding the development in the Lagrangian, tangent cone, and constraint qualifications. It defines constrained problems as a structured type, encodes feasible sets and local minima, and formalizes the geometric and linearized notions that connect the tangent cone to feasible directions. Building on this, the Farkas lemma is formalized to enable rigorous KKT proofs, followed by a complete presentation of the KKT conditions under LICQ or LinearCQ. The dual problem and weak duality are also formalized, providing a verified framework for primal–dual analysis. Overall, the paper delivers a reusable Lean4 toolkit for rigorous optimization proofs and paves the way for extensions to additional constraint qualifications and higher-order conditions.

Abstract

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.

Formalization of Optimality Conditions for Smooth Constrained Optimization Problems

TL;DR

This work presents a Lean4 formalization of first-order optimality conditions for smooth constrained optimization, grounding the development in the Lagrangian, tangent cone, and constraint qualifications. It defines constrained problems as a structured type, encodes feasible sets and local minima, and formalizes the geometric and linearized notions that connect the tangent cone to feasible directions. Building on this, the Farkas lemma is formalized to enable rigorous KKT proofs, followed by a complete presentation of the KKT conditions under LICQ or LinearCQ. The dual problem and weak duality are also formalized, providing a verified framework for primal–dual analysis. Overall, the paper delivers a reusable Lean4 toolkit for rigorous optimization proofs and paves the way for extensions to additional constraint qualifications and higher-order conditions.

Abstract

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.

Paper Structure

This paper contains 12 sections, 10 theorems, 24 equations.

Table of Contents

  1. Introduction
  2. Lean preliminaries
  3. A Brief Introduction to Lean
  4. Tangent Cone
  5. Formalization of Constrained Optimization Problem
  6. Constraint Qualifications
  7. Linear Independent Constraint Qualification
  8. Linear Constraint Qualification
  9. Farkas Lemma
  10. KKT Conditions
  11. Duality Property
  12. Conclusion and Future Work

Key Result

Theorem 2

Let $x^\ast$ be a local minimizer of the constrained problem eq: constrained problem. If the objective function $f$ is differentiable at $x^\ast$, then which is equivalent to

Theorems & Definitions (15)

  • Definition 1
  • Theorem 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Theorem 6
  • Theorem 7
  • Definition 8
  • Theorem 9
  • Theorem 10
  • ...and 5 more