integer programming

Stream: general

[heitopai]

Is there a library for integer programming? I can't find any related ones

[Mirek Olšák]

I don't think there would be a library. The omega tactic implements some integer programming on its own, perhaps part of it could be reused for your purposes but it might be far-fetched (it was not the original intention of the tactic).
https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Omega/Core.lean

[Kim Morrison]

Please try to use cutsat (this will be renamed to lia in v4.27.0-rc1 in two weeks) in preference to omega. Currently its proving power is slightly incomparable with omega, but will hopefully soon be strictly more powerful. In the long run we would like to reduce the outside world's reliance on omega, because the implementation is not as maintainable as we would like.

[Shreyas Srinivas]

You might want to build on @Martin Dvořák 's work. I think one of his repositories is about linear programming and that should give you a good headstart

[Martin Dvořák]

Do you want to build the theory of integer programming, or do you want to use ILP-based proof automation in other formalizations?

In the former case, just import https://github.com/madvorak/duality/blob/main/Duality/LinearProgrammingB.lean and instantiate R with Nat or Int (better is Int because it will allow you to call StandardLP.weakDuality and related stuff).

[Martin Dvořák]

If you want LP with equalities rather than inequalities, just wait a few days — I will be updating https://github.com/madvorak/vcsp/blob/main/VCSP/LinearProgrammingC.lean soon.