Lean의 도움으로 Tao Zhexuan은 새로운 프로젝트를 시작했습니다.
"Alex Kontorovich와 제가 주도하는 새로운 Lean 형식화 프로젝트가 방금 공식적으로 발표되었습니다. 이 프로젝트의 목표는 소수 정리(PNT)의 증명과 그에 수반되는 콤플렉스를 형식화하는 것입니다. 지원 메커니즘을 분석하고 분석합니다. 유명한 수학자 타오저쉬안(Tao Zhexuan)은 자신의 개인 블로그에 정수론의 연구를 진행하고 체보타레프의 밀도 정리와 같은 추가 결과를 제공할 계획이라고 밝혔다. 
소수 정리는 수학에서 중요한 정리로, 자연수 사이의 소수 분포를 설명합니다. 이 정리는 정수론의 중요한 연구 방향입니다. 정식 증명은 본질적으로 컴퓨터 프로그램이지만 C++ 또는 Python의 기존 프로그램과 달리 증명 도우미(예: Lean 언어)를 사용하여 증명의 정확성을 확인할 수 있습니다. 예를 들어, Terence Tao가 자신의 논문 "A MACLAURIN TYPE INEOUALITY"에서 제시한 증명은 한 페이지도 안 되지만 형식 증명에서는 200줄의 Lean 언어를 사용합니다. 
Tao의 공동 연구자인 Alex Kontorovich도 매우 유명한 수학자이며 현재 Rutgers University 수학과의 저명한 교수입니다. 그의 주요 연구 방향은 정수론입니다. 
현재 이 두 수학자가 협업한 Lean 형식화 프로젝트 "PrimeNumberTheoremAnd"가 GitHub에 업로드되었습니다. 
프로젝트 주소: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd프로젝트가 막 시작되었기 때문에 Tao Zhexuan과 Alex Kontorovich도 이에 대한 청사진을 만들었습니다. 
Blueprint 주소 : https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/청사진에는 5개 부분이 포함되어 있음을 알 수 있습니다. 첫 번째 부분에서는 프로젝트의 주요 목표를 소개합니다. 린 정리의 숫자. 그들은 이 문제가 Wiedijk의 공식화를 요구하는 100가지 정리 목록에서 뛰어난 문제 중 하나로 남아 있다고 말합니다. PNT가 이전에 Avigad et al.에 의해 Isabelle에서 공식화되었다는 점은 주목할 가치가 있습니다. 그리고 이 프로젝트의 목표는 이 작업을 소수 계열(디리클레의 정리), 체보타레프의 밀도 정리 등으로 확장하는 것입니다. 현재 위의 목표를 달성하기 위해 다음 세 가지 방법을 고려할 수 있습니다. 가장 빠른 방법은 Michael Stoll이 제안한 "Eulerian Product" 프로젝트입니다. 이 프로젝트의 PNT 증명에는 Wiener가 부족합니다. -Ikehara Tauberian 정리(두 번째 부분에 해당). 두 번째는 점근 공식(세 번째 부분에 해당)만 포함하는 소수 정리(PNT)의 증명을 도출하기 위해 직사각형의 잔차 미적분, 인수 원리 및 멜린 변환을 포함한 일부 복잡한 분석을 개발하는 것입니다. 세 번째 방법은 Hadamard 인수분해 정리, Hoffstein-Lockhart 및 기타 프로세스(네 번째 부분에 해당)를 포함하여 세 가지 방법 중 가장 일반적입니다. 사실 Tao Zhexuan의 이전 연구를 되돌아보면 그는 Lean을 여러 번 언급했습니다. 간단히 말해서 Lean은 수학자들이 정리를 검증하고 사용자가 증명을 작성하고 검증할 수 있도록 돕는 프로그래밍 언어입니다. 원래 Lean과 비교하여 최신 Lean 4 버전은 더 빠른 컴파일러, 향상된 오류 처리, 외부 도구와의 더 나은 통합을 포함하여 많은 최적화가 이루어졌습니다. 이제 테렌스 타오(Terence Tao)와 다른 사람들은 소수 정리의 형식적 증명을 위해 이 도구를 사용했습니다. 린(Lean)이 수학적 연구에서 강력한 조력자가 되었음을 알 수 있습니다. 위 내용은 Tao Zhexuan의 새로운 프로젝트: Lean에서 소수 정리 증명, 연구 청사진 준비 완료의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!
