combinatorial optimization theory in lean

Stream: new members

[Asei Inoue]

Are there any examples of formalizing the theory of combinatorial optimization in Lean? In particular, are there any examples of formalizing results on approximation algorithms? If not, what are the difficulties?

[Martin Dvořák]

Are you interested in doing combinatorial optimization with complexity of algorithms being in the picture?

[Martin Dvořák]

First I should have probably asked if you want to implement stuff or prove stuff.

[Asei Inoue]

I am interested not in the complexity of the algorithm, but in the implementation of concepts such as combinatorial problems, their feasible solutions, optimal solutions, and approximation rates, and whether the approximation rate of a particular algorithm can be proven.

[Martin Dvořák]

Unfortunately, I am not aware of any such effort in Lean.
If you find something, let me know!
Do you have a particular project in mind you would like to work on?

[Asei Inoue]

If you find something, let me know!

Thanks for checking it out .... I understand.

Do you have a particular project in mind you would like to work on?

I think graph theory algorithms are difficult because of their data structure, and I think problems like the Bin Packing Problem have relatively few non-essential difficulties. I would like to start from such a problem.

[Martin Dvořák]

FYI, I have just started with combinatorial optimization theory:
https://github.com/leanprover-community/mathlib4/pull/7404

I define VCSP (general valued constraint satisfaction problems) which is a unifying framework that generalizes both decision problems and optimization problems.

I don't have anything more at the moment, just the first definition.

[Martin Dvořák]

I added some more definitions. At this point, I should probably move it to the "PR reviews" stream.