Duality theory in linear optimization and its extensions -- formally verified

Cet article présente la formalisation en Lean 4 de plusieurs théorèmes de type Farkas sur les corps ordonnés et l'extension de la théorie de la dualité en optimisation linéaire aux coefficients infinis.

L'essentiel

Voici une explication de cet article scientifique, imagée et simplifiée, comme si nous en discutions autour d'un café.

🧱 Le Grand Jeu de l'Équilibre : Quand les Mathématiques deviennent un Code Infaillible

Imaginez que vous êtes un architecte chargé de construire un gratte-ciel. Vous avez une liste de règles strictes : "Le bâtiment ne doit pas pencher de plus de 2 degrés", "Le coût ne doit pas dépasser 10 millions", "Il faut au moins 500 fenêtres".

En mathématiques, c'est ce qu'on appelle un système d'inégalités. La question fondamentale est simple : Est-il possible de construire ce bâtiment ? Ou bien, les règles sont-elles si contradictoires que le projet est impossible dès le départ ?

C'est ici qu'intervient la théorie de la dualité (le sujet de l'article). Elle nous dit quelque chose de magnifique :

"Soit vous pouvez construire le bâtiment (il existe une solution), soit vous pouvez prouver mathématiquement que c'est impossible en mélangeant vos règles pour obtenir une absurdité totale (comme dire '0 est plus grand que 0')."

C'est comme si, au lieu de chercher la solution, vous cherchiez la preuve que le problème est "cassé". L'article de Martin Dvorak et Vladimir Kolmogorov vient dire : "Nous avons écrit un programme informatique qui vérifie cette logique, et il ne se trompe jamais."

---

🤖 Le Gardien de Vérité (Lean 4)

Pourquoi écrire un article entier sur des théorèmes connus ? Parce que les mathématiques sont souvent écrites à la main, avec des mots. Parfois, un humain peut faire une erreur de logique, ou passer à côté d'un détail subtil.

Les auteurs ont utilisé un langage spécial appelé Lean 4. Imaginez Lean comme un gardien de vérité ultra-scrupuleux.

• Vous ne pouvez pas lui dire "ça marche probablement".
• Vous devez lui donner chaque étape de votre raisonnement, comme si vous expliquiez à un robot très intelligent mais très rigide comment faire un nœud de cravate.
• Si une seule étape est floue, le robot refuse de valider le théorème.

Dans cet article, ils ont demandé à ce robot de vérifier les règles du jeu de l'optimisation linéaire (la recherche du meilleur résultat possible sous contraintes). Le robot a dit : "C'est bon, tout est logique. Aucune faille."

---

🌌 L'Innovation : Quand le "Prix" devient Infini

Jusqu'à présent, les mathématiques classiques travaillaient avec des nombres normaux (1, 5, 100, -3, etc.). Mais dans la vraie vie, certaines contraintes sont absolues.

Prenons l'exemple du "déjeuner bon marché" décrit dans l'article :

• Vous voulez manger du riz et des lentilles.
• Le riz coûte 0,92 €.
• Les lentilles coûtent 1,75 €.
• Vous voulez au moins 30g de protéines.

C'est un problème classique. Mais imaginez maintenant que les lentilles sont en rupture de stock.
Comment modéliser cela mathématiquement ?

• L'ancienne méthode : "Disons que les lentilles coûtent 999 999 €". C'est malin, mais c'est un "truc" d'ingénieur. Ce n'est pas élégant.
• La méthode de l'article : Disons que les lentilles coûtent l'Infini (⊤).

C'est là que l'article devient révolutionnaire. Les auteurs ont étendu les mathématiques pour accepter l'Infini et le Moins Infini (⊥) comme des nombres valides dans leurs calculs.

• Si vous essayez d'acheter des lentilles à l'infini, votre budget devient infini.
• Le robot (Lean) a dû vérifier que les règles de l'arithmétique fonctionnent encore avec ces nombres bizarres (par exemple, que "Infini + Moins Infini" ne crée pas de chaos).

Ils ont prouvé que même avec ces nombres "extrêmes", la dualité fonctionne toujours : soit vous trouvez un repas bon marché, soit vous prouvez qu'il est impossible de respecter les règles de nutrition sans payer l'infini.

---

🧩 Les Analogies Clés

1. Le Théorème de Farkas (Le Détective) :
   Imaginez un détective qui reçoit une liste de témoignages contradictoires. Le théorème dit : "Soit les témoignages racontent une histoire cohérente (il y a une solution), soit le détective peut les mélanger pour prouver qu'ils se contredisent eux-mêmes (il y a une preuve d'impossibilité). Il n'y a pas de troisième option."

2. La Dualité (Les Deux Faces d'une Pièce) :
   Pensez à un problème d'optimisation comme une pièce de monnaie.

   • Face : Vous essayez de minimiser le coût (le prix du déjeuner).
   • Pile : Vous essayez de maximiser la valeur des ingrédients (combien vaut chaque gramme de protéine ?).
     L'article prouve que ces deux faces sont parfaitement liées. Si vous connaissez le prix optimal du déjeuner, vous connaissez automatiquement la valeur "ombre" de chaque ingrédient.

3. Lean 4 (Le Traducteur Universel) :
   C'est comme un traducteur qui ne tolère aucune ambiguïté. Si vous dites "environ 5", il vous renvoie. Il faut dire "exactement 5". En forçant les mathématiciens à être précis, ils évitent les erreurs subtiles qui pourraient passer inaperçues dans un papier classique.

---

🏁 En Résumé

Cet article est une victoire de la rigueur.

1. Ils ont vérifié des règles mathématiques fondamentales (les théorèmes de Farkas) avec un ordinateur pour s'assurer qu'elles sont absolument vraies.
2. Ils ont étendu ces règles pour inclure des situations extrêmes (des coûts infinis), ce qui est très utile pour les problèmes réels où certaines contraintes sont "non négociables".
3. Ils ont ouvert la voie à une nouvelle façon de faire des mathématiques : écrire des preuves qui sont aussi fiables que du code informatique.

C'est comme si, après des siècles de calculs à la main, nous avions enfin construit un GPS mathématique qui nous garantit que nous ne nous perdrons jamais, même dans les territoires les plus étranges de l'infini.

Résumé technique

Voici un résumé technique détaillé de l'article « Duality theory in linear optimization and its extensions: formally verified » (Théorie de la dualité en optimisation linéaire et ses extensions : vérifié formellement) par Martin Dvorak et Vladimir Kolmogorov.

1. Problématique et Contexte

L'article s'attaque à la formalisation rigoureuse de la théorie de la dualité en optimisation linéaire, un pilier fondamental des mathématiques appliquées et de l'informatique théorique. Le problème central est double :

1. Vérification formelle : Bien que les théorèmes de dualité (comme le lemme de Farkas et la dualité forte) soient bien connus, leur preuve formelle dans des assistants de preuve modernes (ici Lean 4) reste un défi, notamment pour garantir l'absence d'erreurs dans des raisonnements complexes impliquant des structures algébriques abstraites.
2. Extension aux coefficients infinis : Dans de nombreux problèmes d'optimisation discrets (notamment avec des contraintes « dures »), il est naturel de modéliser certaines contraintes comme impossibles à satisfaire en utilisant des coefficients infinis. Cependant, la théorie classique de la programmation linéaire (PL) ne supporte pas les valeurs infinies ($\infty, -\infty$) car elles brisent la structure de corps (notamment les règles d'arithmétique comme $0 \cdot \infty$). L'objectif est d'étendre la théorie de la dualité à un cadre où les coefficients peuvent prendre des valeurs dans un corps linéairement ordonné étendu ($F_\infty$).

2. Méthodologie

Les auteurs ont utilisé Lean 4 et sa bibliothèque mathématique Mathlib pour formaliser et prouver leurs résultats.

• Cadre Algébrique : Au lieu de se limiter aux réels ($\mathbb{R}$), ils ont travaillé sur des corps linéairement ordonnés ($F$) et des anneaux de division linéairement ordonnés ($R$). Cela permet des résultats plus généraux. Ils ont également défini des modules sur ces anneaux pour traiter des vecteurs et des applications linéaires de manière abstraite.
• Extension des Corps ($F_\infty$) : Ils ont défini une structure $F_\infty = F \cup \{\bot, \top\}$ (où $\bot$ représente $-\infty$ et $\top$ représente $+\infty$).
  • L'arithmétique est définie de manière non standard pour gérer les cas limites : par exemple, $\bot + \top = \bot$ et $0 \cdot \bot = \bot$.
  • Cette structure n'est plus un corps ni même un groupe, mais un monoïde abélien linéairement ordonné dense.
  • Des préconditions strictes ont été établies pour éviter les indéterminations (ex: une ligne ne peut pas contenir à la fois $\bot$ et $\top$).
• Stratégie de Preuve :
  • Ils ont prouvé d'abord une généralisation du lemme de Farkas due à Bartl (valable pour des anneaux de division et des modules infinis), en utilisant une induction sur la taille de l'ensemble des variables.
  • Ensuite, ils ont étendu ces résultats à $F_\infty$ en réduisant le problème à des cas finis par élimination de lignes/colonnes triviales ou contradictoires.
  • La preuve de la dualité forte repose sur le lemme de Farkas étendu et une analyse cas par cas de la faisabilité et de la bornitude des programmes linéaires (PL) et de leurs duaux.

3. Contributions Clés

L'article apporte plusieurs contributions majeures à la fois théoriques et informatiques :

1. Preuve formelle de théorèmes existants :

   • Ils ont formalisé et prouvé le lemme de Farkas (égalités et inégalités) et le théorème de dualité forte de la programmation linéaire standard dans Lean 4.
   • Ils ont prouvé une version généralisée du lemme de Farkas (théorème de Bartl) pour des structures non commutatives et des systèmes infinis d'équations.

2. Nouvelle théorie de la dualité pour les coefficients infinis :

   • Ils ont introduit et prouvé un lemme de Farkas étendu (extendedFarkas) pour $F_\infty$. Ce théorème établit que soit un système d'inégalités a une solution, soit il existe une combinaison linéaire des inégalités menant à une contradiction ($0 < 0$), même avec des coefficients infinis, sous réserve de conditions de cohérence spécifiques.
   • Ils ont défini la notion de Programme Linéaire Valide (ValidELP) sur $F_\infty$, incluant six conditions nécessaires pour éviter les paradoxes arithmétiques.
   • Ils ont prouvé le théorème de dualité forte étendu (ValidELP.strongDuality), établissant que pour un PL valide et son dual, si l'un est réalisable, alors les valeurs optimales sont opposées ($P^* = -D^*$).

3. Développement de bibliothèques Lean :

   • Création d'opérateurs de multiplication matrice-vecteur généralisés (hetero_matrix_products) permettant de multiplier des matrices à valeurs dans $F_\infty$ par des vecteurs à valeurs dans $F$.
   • Définition rigoureuse de la sémantique des programmes linéaires étendus (faisabilité, bornitude, optimum) et de leur dualité.

4. Résultats Principaux

• Théorème 1.4 à 1.6 (Généralisations de Farkas) : Preuve formelle que pour des anneaux de division ordonnés et des modules, l'existence d'une solution à un système linéaire est équivalente à l'impossibilité de dériver une contradiction par combinaison linéaire.
• Théorème 1.8 (extendedFarkas) : Établissement de la dichotomie de Farkas pour les matrices à coefficients dans $F_\infty$, avec des conditions précises sur la présence de $\bot$ et $\top$.
• Théorème 1.11 (ValidELP.strongDuality) : Preuve que pour tout programme linéaire valide sur $F_\infty$, la valeur optimale du primal et celle du dual sont liées par $P^* = -D^*$, dès lors qu'au moins l'un des deux est réalisable.
• Contre-exemples (Section 7) : Les auteurs démontrent que chaque condition de validité (six au total) est nécessaire. L'omission d'une seule condition (ex: présence de $\bot$ et $\top$ dans la même ligne) rend le théorème faux, comme le montrent des contre-exemples explicites.
• Exemple concret (Section 1.2.1) : Application au problème du « déjeuner bon marché ». L'article montre comment modéliser l'indisponibilité d'un ingrédient (lentilles) en augmentant son coût à l'infini ($\top$), permettant de résoudre le problème sans modifier la structure de la matrice, contrairement aux approches numériques classiques.

5. Signification et Impact

• Rigueur Mathématique : Ce travail fournit une base de vérité absolue pour les théorèmes de dualité, éliminant tout risque d'erreur humaine dans les preuves complexes impliquant des cas limites et des structures algébriques abstraites.
• Avancée pour l'Optimisation : En formalisant la gestion des contraintes « dures » via des coefficients infinis, l'article offre un cadre mathématique propre pour les problèmes d'optimisation mixte (contraintes dures vs objectives souples), évitant les heuristiques numériques (comme l'utilisation de grands nombres finis à la place de l'infini).
• Contribution à l'Écosystème Lean/Mathlib : L'article enrichit la bibliothèque Mathlib avec des structures algébriques avancées (anneaux de division ordonnés, modules ordonnés) et des définitions de programmes linéaires étendus. Il démontre également les limites actuelles de l'automatisation de Lean 4 (notamment pour les analyses de cas complexes et la recherche de contre-exemples), tout en validant son efficacité pour l'organisation et la preuve de théorèmes mathématiques élégants.

En résumé, cet article réussit à unifier la théorie classique de la dualité linéaire avec des extensions nécessaires pour l'optimisation moderne, le tout avec un niveau de certitude formelle inédit grâce à l'assistant de preuve Lean 4.