We aim to formalize the broad area of mathematical optimization including convex analysis, convex optimization, nonlinear programming, integer programming and etc in Lean4. Related topics include but are not limited to the definition and properties of convex and nonconvex functions, optimality conditions, convergence of various algorithms.

More topics related to computational mathematics such as numerical linear algebra and numerical analysis will be included in the future.

Our github web page corresponding to this work can be found at here .

Lean4 Toolchain Installation

How to use the code in this repository

If anything goes wrong, please feel free to contact Chenyi Li through email (lichenyi@stu.pku.edu.cn).

The version of Lean4 that used by this repository can be checked here.

Use the Convex library as a Lean4 project dependency

In a Lean4 project, add these lines to your lakefile.lean:

require convex from git

The convex library uses mathlib4 as a dependency, command lake exe cache get can be used to fetch mathlib4 cache.

Contribute to the Convex library

The command

git clone https://github.com/optsuite/optlib.git && cd optlib && code .

will download the source of the convex library. After editing those files, you can fork this project on GitHub and file a pull request.

What we have done





What we plan to do

Convex Analysis

  • First Order Conditions for Convex Functions (Done)
  • Second Order Conditions for Convex Functions
  • Definition and Properties of Strongly Convex Functions (Done)
  • Definition and Properties of L-smooth Functions (Done)
  • Definition and Properties of Subgradients (Done)
  • ......

Optimality Conditions

  • First Order Conditions for Constrained and Unconstrained Methods
  • Second Order Conditions for Constrained and Unconstrained Methods
  • KKT conditions
  • ......

Convergence of Optimization Algorithms

  • Gradient Descent for Convex and Strongly Convex Functions (Done)
  • Line Search Methods
  • Subgradient Methods (Done)
  • Proximal Gradient Methods (Done)
  • Nesterov Acceleration Method (Done)
  • ADMM Methods
  • ......

Many other things to be added ...


The Team

We are a group of scholars and students with a keen interest in mathematical formalization.


Other Contributors

  • Undergraduate students from Peking University:

    Hongjia Chen, Wanyi He, Yuxuan Wu, Shengyang Xu, Junda Ying, Penghao Yu, ...

  • Undergraduate students from Summer Seminar on Mathematical Formalization and Theorem Proving, BICMR, Peking University, 2023:

    Zhipeng Cao, Yiyuan Chen, Heying Wang, Zuokai Wen, Mingquan Zhang, Ruichong Zhang, ...

  • Other collaborators:

    Anjie Dong, ...


Copyright (c) 2024 Chenyi Li, Ziyu Wang, Zaiwen Wen. All rights reserved.

Released under Apache 2.0 license as described in the file LICENSE.