Mit Hilfe von Lean startete Tao Zhexuan ein neues Projekt.
„Ein neues Lean-Formalisierungsprojekt unter der Leitung von Alex Kontorovich und mir wurde gerade offiziell angekündigt. Das Projekt zielt darauf ab, den Beweis des Primzahlsatzes (PNT) und den dazugehörigen komplexen Supportmechanismus zu formalisieren und zu analysieren.“ der Zahlentheorie und planen, weitere Ergebnisse wie Chebotarevs Dichtesatz zu liefern“, schrieb der berühmte Mathematiker Tao Zhexuan in seinem persönlichen Blog. 
Der Primzahlsatz ist ein wichtiger Satz in der Mathematik. Er beschreibt die Verteilung von Primzahlen unter natürlichen Zahlen. Dieser Satz ist eine wichtige Forschungsrichtung in der Zahlentheorie. Ein formaler Beweis ist im Wesentlichen ein Computerprogramm, aber im Gegensatz zu herkömmlichen Programmen in C++ oder Python kann die Richtigkeit des Beweises mithilfe eines Beweisassistenten (z. B. der Lean-Sprache) überprüft werden. Beispielsweise umfasst der Beweis, den Terence Tao in seinem Aufsatz „A MACLAURIN TYPE INEOUALITY“ liefert, weniger als eine Seite, aber der formale Beweis verwendet 200 Zeilen Lean-Sprache. 
Alex Kontorovich, Taos Mitarbeiter, ist ebenfalls ein sehr berühmter Mathematiker und derzeit ein angesehener Professor am Fachbereich Mathematik der Rutgers University. Sein Forschungsschwerpunkt ist die Zahlentheorie. 
Derzeit wurde das von diesen beiden Mathematikern gemeinsam entwickelte Lean-Formalprojekt „PrimeNumberTheoremAnd“ auf GitHub hochgeladen. 
Projektadresse: https://github.com/AlexKontorovich/PrimeNumberTheoremAndDa das Projekt gerade erst gegründet wurde, erstellten Tao Zhexuan und Alex Kontorovich auch eine Blaupause dafür: 
Blaupausenadresse : https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/Es ist ersichtlich, dass die Blaupause 5 Teile enthält: Der erste Teil stellt das Hauptziel des Projekts vor: den Nachweis von Primzahlen Zahlen im Lean-Theorem. Sie sagen, das Problem bleibe eines der herausragenden auf Wiedijks Liste der 100 Theoreme, die einer Formalisierung bedürfen. Es ist erwähnenswert, dass PNT bereits früher formalisiert wurde, und zwar in Isabelle von Avigad et al. Und das Ziel dieses Projekts ist es, diese Arbeit auf Primzahlen in Reihen (Satz von Dirichlet), den Dichtesatz von Chebotarev und mehr auszudehnen. Derzeit können die folgenden drei Methoden in Betracht gezogen werden, um die oben genannten Ziele zu erreichen: Das schnellste ist das von Michael Stoll vorgeschlagene Projekt „Eulerian Product“, dem nur der Wiener fehlt -Theorem von Ikehara Tauber (Entsprechend dem zweiten Teil). Die zweite besteht darin, eine komplexe Analyse zu entwickeln, einschließlich Residuenrechnung auf Rechtecken, Argumentationsprinzip und Mellin-Transformation, um einen Beweis des Primzahlsatzes (PNT) abzuleiten, der nur asymptotische Formeln enthält (entsprechend dem dritten Teil). Die dritte Methode ist auch die gebräuchlichste der drei Methoden, einschließlich des Hadamard-Faktorierungssatzes, Hoffstein-Lockharts und anderer Prozesse (entsprechend dem vierten Teil). Der letzte Teil ist die grundlegende Schlussfolgerung. Tatsächlich erwähnte Tao Zhexuan im Rückblick auf frühere Forschungen Lean oft. Einfach ausgedrückt ist Lean eine Programmiersprache, die Mathematikern bei der Überprüfung von Theoremen hilft, wobei Benutzer Beweise schreiben und überprüfen können. Im Vergleich zum ursprünglichen Lean verfügt die neueste Lean 4-Version über zahlreiche Optimierungen, darunter einen schnelleren Compiler, eine verbesserte Fehlerbehandlung und eine bessere Integration mit externen Tools. Nun haben Terence Tao und andere dieses Werkzeug für den formalen Beweis des Primzahlsatzes verwendet. Es ist ersichtlich, dass Lean zu einem leistungsstarken Assistenten in der mathematischen Forschung geworden ist. Das obige ist der detaillierte Inhalt vonTao Zhexuans neues Projekt: Der Beweis des Primzahlsatzes in Lean, der Forschungsentwurf ist fertig. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!
