FORMAL

Avec FORMAL, nous implémenterons des algorithmes d'apprentissage automatique et les preuves mathématiques de leurs performances dans le même langage de programmation et de preuve, Lean. Le but est de permettre à des IA d'inventer de nouveaux algorithmes et de fournir des preuves théoriques de leurs propriétés. Avoir accès non seulement au code de l'algorithme mais aussi à la théorie qui a mené à sa création permettra à une IA d'apprendre à améliorer ces deux aspects en tandem, pour créer de meilleurs algorithmes d'apprentissage automatique.