테렌스 타오(terence tao)가 인터넷에서 가장 강력한 두뇌를 가진 사람에게 보상을 제공하고 있습니다! ai 인간이 수학 문제를 전복시킨다? 베르사유 네티즌들은 사라졌다
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
[새로운 지혜 소개]최근 tao zhexuan은 대다수의 네티즌과 수학 매니아를 대상으로 다음과 같은 도전 과제를 시작했습니다. 인기 수학 매니아, 증명 보조자, 자동화 보조자 및 ai가 힘을 합쳐 몇 자릿수까지 확장되는 수학 문제를 증명할 수 있을까요?
terence tao가 시작한 "크라우드소싱" 수학 연구 프로젝트에 참여하고 싶으신가요?ai를 활용한 증명 수학적 연구는 점점 더 실현 가능해지고 있습니다.
그들 각각은 서로의 기여를 검증할 만큼 프로젝트 측면에 대해 충분히 잘 알고 있습니다.그러나 대규모 수학 연구 프로젝트, 특히 공공 기여가 포함된 프로젝트를 조직하려는 경우 훨씬 더 번거롭습니다.그 이유는 모든 사람의 기여도를 검증하기 어렵기 때문입니다.2023년 말, 테렌스 타오는 다항식 프레이만-루자 추측의 증명을 공식화한 lean4 프로젝트가 3주 만에 성공했다고 발표했습니다. (사진은 최근 현황입니다.)수학적 논증 중 한 부분의 실수로 전체 프로젝트가 실패할 수 있다는 점에 유의하세요.더욱이, 일반적인 수학 프로젝트의 복잡성을 고려할 때, 학부 수학 교육을 받은 일반 대중이 의미 있는 기여를 하리라 기대하는 것은 비현실적입니다.이를 통해 우리는 ai 도구를 수학 연구 프로젝트에 통합하는 것도 매우 어렵다는 것을 알 수 있습니다.ai는 합리적으로 보이지만 실제로는 말이 되지 않는 주장을 생성할 수 있으므로 ai 생성 부분을 프로젝트에 추가하기 전에 추가 검증이 필요합니다.다행스럽게도 lean과 같은 증명 지원 언어는 이러한 장애물을 극복하고 전문 수학자, 일반 대중 및 ai 도구 간의 협업을 가능하게 하는 잠재적인 방법을 제공합니다.이 접근 방식은 전체 프로젝트를 이해하지 않고도 프로젝트를 모듈식 방식으로 완료할 수 있는 작은 부분으로 나눌 수 있다는 전제를 기반으로 합니다.현재 사례에는 주로 기존 수학적 결과를 공식화하는 프로젝트(예: 최근 marton이 증명한 pfr 추측의 공식화)가 포함됩니다.이러한 공식화는 주로 인간 기여자(전문 수학자 및 관심 있는 대중 포함)의 크라우드소싱을 통해 수행됩니다.동시에 전통적인 자동 정리 증명자 및 보다 현대적인 ai 기반 도구를 포함하여 작업을 완료하기 위해 보다 자동화된 도구를 도입하려는 새로운 시도도 있습니다.새로운 수학적 문제를 탐구하는 것이 가능해진다
그리고,테렌스 타오또한 이 새로운 패러다임은 기존 수학을 형식화하는 것뿐만 아니라 완전히 새로운 수학을 탐구하는 데에도 사용될 수 있다고 믿어집니다!과거 그와 그의 후계자는 온라인 협업 "polymath" 프로젝트를 조직했는데, 이는 좋은 예입니다.그러나 이 프로젝트는 증명 보조 언어를 워크플로에 통합하지 않았으며 기여를 인간 조정자가 관리하고 검증해야 했기 때문에 시간이 많이 걸리고 프로젝트의 추가 확장이 제한되었습니다.이제 tao zhexuan은 증명 보조 언어를 추가하면 이러한 병목 현상을 해결할 수 있기를 바라고 있습니다.그는 특히 한 번에 한두 가지 문제에만 초점을 맞추는 대신 이러한 최신 도구를 사용하여 다양한 수학적 문제를 동시에 탐색할 수 있는지 여부에 관심이 있습니다.본질적으로 이 접근 방식은 반복적인 작업을 위한 모듈식이며, 모든 기여를 엄격하게 조정하는 플랫폼이 있는 경우 크라우드소싱 및 자동화 도구가 특히 유용할 수 있습니다.이러한 유형의 수학적 문제는 이전 방법으로는 확장할 수 없었습니다. 이런 종류의 문제에 대해 합리적인 직관을 얻을 때까지 수년에 걸쳐 개별 논문을 통해 한 번에 하나의 데이터 포인트를 천천히 탐색하지 않는 한.또한, 대규모 문제 데이터 세트가 있으면 다양한 자동화 도구의 성능 평가를 수행하고 다양한 워크플로의 효율성을 비교하는 데 도움이 될 수 있습니다.올해 7월에는 비지비버 5번째 숫자가 47,176,870으로 확인됐다.gimps(great internet mersenne prime search)와 같은 일부 초기 크라우드소싱 컴퓨팅 프로젝트는 보조 언어를 증명하는 대신 보다 전통적인 작업 증명 메커니즘을 사용하지만 정신 면에서는 이러한 프로젝트와 유사합니다.terence tao는 수학적 공간을 탐구하는 크라우드소싱 프로젝트의 다른 기존 사례가 있는지, 그리고 사용할 수 있는 교훈이 있는지 알고 싶다고 말했습니다.tao zhexuan은 새로운 프로젝트를 제안합니다
이를 위해 tao는 이 패러다임을 추가로 테스트하기 위한 프로젝트를 직접 제안했습니다.이 프로젝트는 작년 mathoverflow 질문에서 영감을 받았습니다.얼마 지나지 않아 tao zhexuan은 mathstodon에서 이에 대해 더 자세히 논의했습니다.이 문제는 보편대수학 분야에 속하며 원래 그룹(마그마)의 단순 방정식 이론에 대한 중간 규모 탐구를 포함합니다.원래 그룹은 이진 연산을 갖춘 그룹입니다.세트 g.처음에 이 연산 o에는 추가 공리가 붙어 있지 않으므로 원래 그룹 자체는 비교적 간단한 구조입니다.물론 항등 공리나 결합성 공리와 같은 추가 공리를 추가하면 그룹, 반그룹 또는 모노이드와 같은 더 친숙한 수학적 객체를 얻을 수 있습니다.여기서 우리는 평등의 (상수가 없는) 공리에 관심이 있습니다. 이러한 공리는 연산 o와 g의 하나 이상의 알려지지 않은 변수로 구성된 표현식의 동일성과 관련됩니다.이러한 공리의 두 가지 친숙한 예는 교환 법칙 xoy = yox와 결합 법칙(xoy) oz = xo(yoz)입니다.여기서 x, y, z는 원래 그룹 g의 알 수 없는 변수입니다.반면에 (왼쪽) 항등 공리 eox = x는 상수 e ∈ g를 포함하기 때문에 여기서 방정식 공리로 간주되지 않습니다. 상수와 관련된 공리는 이 연구에서 논의되지 않습니다.다음으로, 자신이 시작한 연구 프로젝트를 설명하기 위해 terence tao는 원시 그룹에 대한 평등 공리의 11가지 예를 소개했습니다.이러한 등식 공리는 기본 그룹 연산과 알 수 없는 변수만 포함하는 방정식입니다.예를 들어, 방정식 7은 교환 공리를 나타내고, 방정식 10은 연관 공리를 나타냅니다.상수 공리 방정식 1은 원래 그룹 g가 최대 하나의 요소를 갖도록 제한하기 때문에 가장 강력하며, 반사 공리 방정식 11은 가장 약하고 모든 원래 그룹은 이 공리를 충족합니다.다음으로, 이러한 공리 간의 파생 관계를 탐색할 수 있습니다. 어떤 공리가 어떤 공리를 추론할 수 있습니까?예를 들어, 방정식 1은 이 목록의 다른 모든 공리로 이어지며, 이는 다시 방정식 11로 이어집니다.방정식 8은 방정식 9를 도출하기 위한 특수 사례로 사용될 수 있으며, 이는 다시 방정식 10을 도출하기 위한 특수 사례로 사용될 수 있습니다.이러한 공리 간의 완전한 파생 관계는 다음 hasse 다이어그램으로 설명할 수 있습니다.이 결과는 특히 수학 q&a 웹 사이트 mathoverflow의 질문인 상수 공리(수식 1)와 결합성 공리(수식 10) 사이에 방정식 공리가 있는지 여부에 대한 답변입니다.여기서 암시 관계의 대부분은 증명하기 쉽다는 점은 주목할 가치가 있습니다. 그러나 사소하지 않은 암시 관계가 있습니다.이 관계는 이전 질문과 밀접하게 관련된 mathoverflow 게시물에 대한 답변에서 발견되었습니다.명제 1: 방정식 4는 방정식 7을 의미합니다.증명: g가 방정식 4를 만족한다고 가정합니다.특히, y = xox일 때 (xox) o (xox) = (xox) ox가 됩니다.(1)을 다시 적용하면 xox가 멱등원이라는 결론을 내릴 수 있습니다.이제 (1)에서 x를 xox로 바꾸고 (2)를 사용하면 (xox) oy = yo (xox)를 얻습니다.특히 xox와 yoy는 서로 바꿔 사용할 수 있습니다.게다가 (1)을 두 번 적용하면 (xox) o (yoy) = (yoy) ox = xoy가 됩니다.따라서 (3)은 수학식 7인 xoy = yox로 단순화될 수 있다.위의 논증 과정의 형식화는 lean에서 찾을 수 있습니다.그러나 한 평등 공리 집합이 다른 평등 공리 집합을 결정하는지 여부를 결정하는 일반적인 문제는 결정 불가능하다는 점은 주목할 가치가 있습니다.따라서 여기의 상황은 "busy beaver" 챌린지와 다소 유사합니다. 즉, 특정 복잡성 지점 이후에는 결정할 수 없는 문제에 직면하게 되지만 이 임계값에 도달하기 전에 여전히 흥미로운 문제와 현상을 발견할 수 있기를 바랍니다.위의 hass 다이어그램은 나열된 등식 공리 간의 수반 관계를 주장할 뿐만 아니라 공리 간의 비함축 관계도 주장합니다.예를 들어, 그림에 표시된 대로 교환 공리 방정식 7은 방정식 4(x + x) + y = y + x의 공리를 암시하지 않습니다.이를 증명하려면 가환 공리 방정식 7을 만족하지만 공리 방정식 4를 충족하지 않는 원시 그룹의 예를 찾으십시오.예를 들어, 이 경우 연산이 xoy := x+y인 자연수 집합 n을 선택할 수 있습니다.더 일반적으로, 다이어그램은 (이미 언급한 함축 관계와 함께) 다음 11개의 공리 중 함의 관계의 부분적으로 정렬된 집합을 완전히 설명하는 다음과 같은 비 함축 관계를 주장합니다.여기에서 tao zhexuan은 독자들에게 일부 증명을 완성하기 위한 반례를 제안하도록 초대합니다.가장 찾기 어려운 반례는 방정식 9가 방정식 8을 추론할 수 없다는 것입니다.lean을 사용하여 솔루션을 제공할 수 있습니다.또한 tao zhexuan은 위의 모든 포함 및 포함 방지 관계에 대한 lean 증명이 포함된 github 저장소도 제공합니다.11개 방정식의 haas 다이어그램을 계산하는 것만으로도 이미 약간 번거롭다는 것을 알 수 있습니다.terence tao가 제안한 프로젝트는 더 넓은 범위의 방정식 세트를 포괄하기 위해 이 hass 다이어그램을 몇 배로 확장하려는 시도입니다.그가 제안한 집합은 합 방정식의 반사성 및 대칭성 공리가 다시 명명될 때까지 원래 그룹 연산 o를 최대 4번 사용한 방정식 집합인 ε이었습니다.여기에는 위에서 언급한 11개의 방정식이 포함되지만 더 많은 방정식이 있습니다.카탈로니아어 수 c_n은 이진 연산 o(n+1 자리 표시자 변수에 적용됨)를 사용하여 표현식을 형성하는 방법의 수이고 m개의 자리 표시자 변수 문자열이 주어지면 벨 수 b_m은 이러한 변수가 사용되는 방법의 수입니다. 할당된 이름(레이블을 다시 지정할 수 있음) - 특정 자리 표시자에 동일한 이름을 할당할 수 있습니다.따라서 대칭성을 무시하면 최대 4개의 연산을 포함하는 방정식의 수는 다음과 같습니다.좌변과 우변이 같은 방정식의 수는 다음과 같습니다.나머지 9118개의 방정식은 방정식의 대칭성으로 인해 쌍으로 나타나므로 ε의 전체 크기는 다음과 같습니다.
tao zhexuan은 아직 그러한 id의 전체 목록을 생성하지 않았지만 python을 사용하면 쉽게 수행할 수 있다고 의심합니다.ai 도구를 사용하면 필요한 대부분의 코드를 생성할 수 있습니다.그는 ε의 기하학이 어떤 모습일지 전혀 모른다고 말했습니다.대부분의 방정식은 서로 비교할 수 없습니까? '강한' 공리와 '약한' 공리로 나누어질까요?이제 terence tao의 메시지 영역에는 수십 개의 댓글이 있습니다.관심 있는 독자 여러분, tao zhexuan도 여러분에게 초대장을 보냈습니다.
