Lazi

Problème des fondations

Problème de l'informatisation des mathématiques

Informatiser les mathématiques permet de vérifier les preuves et offre les avantages courants de l'informatisation (base de données, recherche de théorème, vérifications, assistance etc).
Les mathématiques ont déjà une forme d'informatisation avec des logiciels comme Coq, mais on est alors obligé d'avoir en quelque sorte deux mathématiques :

  • La mathématique objet du logiciel (comme la théorie des ensembles).
  • La mathématique du logiciel : ce sont les règles, constructions et raisonnement nécessaire à la production, l'utilisation et l'extension du logiciel.
Avec Lazi ces deux mathématiques sont unifiées car Lazi est en quelque sorte une mathématique "réentrante", c'est à dire que naturellement Lazi a une représentation d'elle même. Cette représentation est avantageusement totale, c'est à dire qu'il est bénéfique que mêmes les parties considérées habituellement comme secondaires (les notations, définitions, déclarations de théorèmes etc) soient intégrées à Lazi.

Il en découle que développer Lazi (grâce aux extensions) revient en même temps à développer un logiciel d'aide à la preuve.

Lazi étant une mathématique constructive, ses extensions sont basées sur la traduction des preuves, ce qui permet de faire le pont entre les différentes mathématiques définies par des extensions. On obtient alors une aide naturelle pour traduire par exemple des preuves en mathématique classique vers Lazi (quand c'est possible) ou encore une preuve en programme informatique.

Problème des extensions

Que ce soit la théorie des catégories ou l'analyse non standard un mathématicien qui fait des mathématiques classiques (ou un logiciel de vérification de preuves en mathématique classique) ne peut accepter les preuves d'autres mathématiques que par un travail "hors système". C'est à dire qu'il doit à un moment donné se placer en dehors du cadre pour faire de la métamathématique afin d'accepter une preuve provenant d'une autre mathématique (même si la vérité prouvée est dans le langage de la mathématique classique).
Cela complique l'utilisation d'autre mathématiques car alors elle ne sont pas forcément reconnues.

Lazi résous ce problème par le fait qu'il intègre un mécanisme d'extensions et de traduction qui permettent de définir, prouver et utiliser des extensions sans sortir de la mathématique. Il n'y a plus alors besoin d'une reconnaissance spéciale ni de passer par de la métamathématique pour utiliser des extensions, même exotiques.

Problème d'unicité

Le mathématique classique (calcul des prédicats etc, théorie des ensembles) s'est répandues non pour des raisons purement scientifiques mais aussi pour des raisons pratiques : elles sont faciles à utiliser et la communauté scientifique a besoin d'unifier ses pratiques.

Il reste néanmoins une question de haut niveau non réglée, que l'on pourrait résumer ainsi : si l'on prend des millions de sociétés isolées au moins aussi intelligentes que l'humanité, existent-il une tendance à la convergence dans le temps des fondations mathématiques utilisées par celles-ci ?

Cette question, par sa formulation, peut sembler purement rhétorique, mais elle permet en fait de se questionner simplement sur la place et la nature des mathématiques. Cette question reste ouverte et elle a un intérêt pratique : si il existe une mathématique "naturelle" alors elle possède des avantages qui la rendent très rentable à utiliser.

Que l'on soit d'un avis ou d'un autre, on peut avoir la curiosité d'explorer suffisamment Lazi pour constater qu'une esthétique (et donc puissance) singulière en émane.