Avec l'aide du Lean, Tao Zhexuan a démarré un nouveau projet.
"Un nouveau projet de formalisation Lean mené par Alex Kontorovich et moi-même vient d'être officiellement annoncé. Le projet vise à formaliser la preuve du théorème des nombres premiers (PNT) et la complexité qui l'accompagne. Analyser et analyser le support mécanisme de la théorie des nombres et envisage de donner d'autres résultats tels que le théorème de la densité de Chebotarev", a écrit le célèbre mathématicien Tao Zhexuan sur son blog personnel. 
Le théorème des nombres premiers est un théorème important en mathématiques. Il décrit la distribution des nombres premiers parmi les nombres naturels. Ce théorème est une direction de recherche importante en théorie des nombres. Une preuve formelle est essentiellement un programme informatique, mais contrairement aux programmes traditionnels en C++ ou Python, l'exactitude de la preuve peut être vérifiée à l'aide d'un assistant de preuve (comme le langage Lean). Par exemple, la preuve donnée par Terence Tao dans son article « A MACLAURIN TYPE INEOUALITY » fait moins d'une page, mais la preuve formelle utilise 200 lignes de langage Lean. 
Alex Kontorovich, collaborateur de Tao, est également un mathématicien très célèbre et est actuellement un professeur distingué au département de mathématiques de l'Université Rutgers. Son principal domaine de recherche est la théorie des nombres. 
Actuellement, le projet formel Lean "PrimeNumberTheoremAnd" collaboré par ces deux mathématiciens a été téléchargé sur GitHub. 
Adresse du projet : https://github.com/AlexKontorovich/PrimeNumberTheoremAndParce que le projet vient d'être créé, Tao Zhexuan et Alex Kontorovich ont également construit un plan pour cela : 
Adresse Blueprint : https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/On peut voir que le plan contient 5 parties : La première partie présente l'objectif principal du projet est de prouver qu'il est premier nombres dans le théorème Lean. Ils disent que le problème reste l'un des plus importants sur la liste de Wiedijk des 100 théorèmes nécessitant une formalisation. Il est à noter que le PNT a été formalisé précédemment, dans Isabelle par Avigad et al. Et le but de ce projet est d'étendre ces travaux aux nombres premiers en séries (théorème de Dirichlet), théorème de densité de Chebotarev, etc. Actuellement, les trois méthodes suivantes peuvent être envisagées pour atteindre les objectifs ci-dessus : Le plus rapide est le projet "Eulerian Product" proposé par Michael Stoll. La preuve du PNT dans ce projet ne manque que le Wiener. -Théorème taubérien d'Ikehara (Correspondant à la deuxième partie). La seconde consiste à développer une analyse complexe, incluant le calcul des résidus sur les rectangles, le principe d'argument et la transformation de Mellin, pour en dériver une preuve du théorème des nombres premiers (PNT) contenant uniquement des formules asymptotiques (correspondant à la troisième partie). La troisième méthode est également la plus courante des trois méthodes, dont le théorème de factorisation d'Hadamard, Hoffstein-Lockhart et d'autres processus (correspondant à la quatrième partie). La dernière partie est l'inférence de base. En fait, en repensant aux recherches précédentes de Tao Zhexuan, il a mentionné Lean à plusieurs reprises. En termes simples, Lean est un langage de programmation qui aide les mathématiciens à vérifier des théorèmes, où les utilisateurs peuvent rédiger et vérifier des preuves. Par rapport au Lean original, la dernière version Lean 4 présente de nombreuses optimisations, notamment un compilateur plus rapide, une gestion améliorée des erreurs et une meilleure intégration avec des outils externes. Aujourd'hui, Terence Tao et d'autres ont utilisé cet outil pour la preuve formelle du théorème des nombres premiers. On peut voir que Lean est devenu un assistant puissant dans la recherche mathématique. Ce qui précède est le contenu détaillé de. pour plus d'informations, suivez d'autres articles connexes sur le site Web de PHP en chinois!
