Une place Lean · Matrices aléatoires
RMTLib
Une place Lean pour les résultats de la théorie des matrices aléatoires.
RMTLib est une place Lean pour les résultats de la théorie des matrices aléatoires : une bibliothèque où énoncés et preuves sur les matrices aléatoires sont écrits en Lean et vérifiés par ordinateur.
La théorie des matrices aléatoires rejoint la théorie des nombres, notamment à travers la statistique des zéros de la fonction zêta de Riemann, dont la thèse de Tate retrouve l'équation fonctionnelle à partir de facteurs locaux en chaque place. Une bibliothèque est un territoire à part entière : un cadre où les résultats sont élaborés en termes locaux précis, puis partagés. Le lien vers RMTLib sera publié ici dès qu'il sera disponible.