vltanh/formalize-math-paper

Lean 4로 수학 논문 형식화하기

다음과 같은 Lean 프로젝트와 관련 문서를 제공합니다:

• 논문이 증명하는 모든 결과는 논문 자체의 논증으로 증명됩니다. 증명이 논문의 증명과 달라져야 하는 경우에만 달라지며, 모든 이탈(departure)은 보고됩니다(규칙, "충실한 증명" 참조).
• 논문이 증명에서 인용하는 모든 결과도 증명됩니다: Mathlib, 다른 공개 라이브러리, 또는 External/ 디렉토리에. 인용된 결과에 필요한 수학이 아직 어떤 Lean 라이브러리에도 없고 프로젝트가 합리적으로 구축할 수 없는 경우, 해당 결과는 이를 사용하는 모든 명제의 명명된 가설(named hypothesis)이 되며, 형식화는 명시적으로 조건부임을 밝힙니다.
• 명제는 논문이 말한 그대로이며, 모든 편차는 문서화됩니다.
• lake build가 성공하며 sorry(설계상 Challenge.lean의 명제는 제외), admit, 프로젝트 axiom이 없습니다. 라이브러리의 모든 선언은 propext, Classical.choice, Quot.sound에만 의존합니다.
• REPORT.md는 형식화 결과를 기준으로 논문을 감사합니다. 이 보고서는 이후 내용으로 끝납니다: 논문 이후 주제가 어떻게 발전했는지, 결과를 어떻게 확장, 일반화 또는 강화할 수 있는지, 증명을 어떻게 단순화할 수 있는지. README.md는 형식화를 요약하고, CREDITS.md는 제작 방식을 설명합니다(절차, 에이전트 및 모델, 시간 및 노력(실행 로그)).
• 사용자가 요청하지 않는 한 절대 공개되지 않는 비공개 NEXT.md는 사용자가 이 논문 다음에 작성할 수 있는 논문에 대해 답변합니다: 각각 독립적인 논문이 될 만한 몇 가지 후보를 깊이 탐구합니다(장애물, 시도, 증거, 이미 증명된 내용). 단순한 점진적 확장 목록이 아닙니다.
• 프로젝트는 Palomar용으로 패키징되며, 사용자의 허락을 받아 Palomar의 사전 점검(preflight)을 통해 게시 및 실행됩니다.

작업은 두 단계로 진행됩니다. 1단계에서는 논문 자체가 증명하는 모든 것을 형식화합니다. 문헌에서 가져온 결과는 임시 공리(axiom)일 수 있습니다. 2단계에서는 해당 공리를 제거합니다: 증명하거나, 도달할 수 없는 결과는 명시된 가설로 전환합니다. 설정은 두 단계 전에 수행되며, 검증, 정리, 감사 및 패키징은 이후에 수행됩니다.

원칙

다음은 아래 규칙을 설명합니다. 규칙이 상황을 다루지 않을 때 사용하십시오.

• 논문은 명제와 논증의 진리의 근원(source of truth)이며, Lean은 정확성을 판단합니다. 논문과 다른 명제는 증명이 아무리 깔끔하더라도 잘못된 형식화입니다. 다른 논증을 통해 논문의 명제에 도달하는 증명도 마찬가지입니다: 형식화는 논문의 주장뿐만 아니라 논문의 증명도 확인합니다. 누군가 증명하기 전에 TeX 소스와 대조하여 명제를 검토하십시오. 증명이 작성된 후에는 논문의 증명과 비교하십시오. 둘 중 어느 것도 묵시적으로 변경하지 마십시오.
• 아무도 컴파일하지 않은 형식화는 초안(draft)입니다. 기억에 의존하여 작성되고 컴파일되지 않은 Lean 코드는 종종 추측된 보조정리 이름, 잘못된 시그니처 및 거짓 도움말 보조정리를 포함합니다. Lean 도구 체인을 사용할 수 있을 때마다 컴파일하십시오. 도구 체인이 없거나 사용자가 컴파일을 금지하는 경우, 결과가 검증되지 않았음을 명확히 밝히십시오.
• "표준적", "자명한", "대칭에 의해", "일상적인"에도 증명이 필요합니다. Mathlib에 사실이 있을 수 있습니다. 없으면 증명하십시오. 논문 자체가 다른 출처에서 가져온 것만 공리가 될 수 있습니다.
• External(외부)은 결과가 어디에서 왔는지를 의미할 뿐, 신뢰할 수 있음을 의미하지 않습니다. 인용된 결과는 그 출처 때문에 External/에 있습니다. 다른 모든 것과 마찬가지로 증명됩니다.
• 가정은 형태와 관계없이 가정입니다. 증명되지 않은 인용 결과는 공리, 가설 또는 구조의 필드로 작성되었는지 여부와 관계없이 가정됩니다. 공리는 허용되지 않습니다. 가설은 명제의 독자가 각 가설을 볼 수 있을 때 허용되며, 가정하는 결과의 이름으로 표시됩니다. 데이터와 가정된 정리를 혼합하는 구조는 결과가 의존하는 것을 숨깁니다. 데이터처럼 보이지만 정리를 보유하는 유형의 매개변수도 마찬가지입니다.
• 데이터는 그 정의 속성과 함께 제공됩니다. 명제가 논문의 객체를 구성하지 않고 매개변수로 받을 때, 해당 객체를 정의하는 속성도 요구해야 합니다. 그렇지 않으면 정리는 다른 가설을 만족하는 모든 객체에 대한 것이며, 이는 다른 명제입니다.
• 표현 선택에는 연결 다리(bridge)가 필요합니다. Lean의 객체는 논문의 객체와 다를 수 있습니다: 1부터 시작하는 인덱스 대신 0부터, 인덱스된 족(family) 대신 리스트, 비공식 객체 대신 번들된 Mathlib 구조체, "동형사상까지" 설명 대신 구체적인 모델. 그럴 때는 둘을 연결하는 보조정리를 증명하고 선택을 문서화하십시오. 두 표현이 동등하다고 가정하지 마십시오.
• 상수와 범위는 수학의 일부입니다. 거듭제곱, 인수, 바닥 함수, 천장 함수, 엄격 부등식 대 완화 부등식, 범위의 끝점, ℕ에서의 절단 뺄셈(truncated subtraction)은 명제의 참 여부를 결정합니다.
• 정직하게 보고하십시오. 단계를 건너뛰었거나, 증명이 실패했거나, 명제를 변경해야 했거나, 증명이 논문과 달라져야 했다면 그 사실과 이유를 말하십시오. 감사는 신뢰할 수 있을 때만 유용합니다.
• 증명의 공백(gap)은 거짓 명제가 아닙니다. 논문의 증명이 가설이 제공하지 않는 사실을 사용할 때, 명제는 여전히 참일 수 있습니다. 명제에 대해 결론을 내리기 전에 올바른 논증을 찾으십시오.
• 작업을 측정하십시오. 독자와 레지스트리는 형식화가 어떻게 만들어졌는지 묻습니다. 답은 작업하면서 기록하는 것은 저렴하지만, 나중에 재구성하는 것은 어렵습니다.

규칙

• 증명을 가능하게 하기 위해 논문 결과의 명제를 절대 약화하거나 변경하지 마십시오. 논문의 명제가 거짓인 경우, 작업을 중단하고 즉시 반례와 함께 사용자에게 알리십시오. 다른 작업은 그동안 계속될 수 있습니다. 사용자가 동의하면 가장 가까운 올바른 버전을 형식화하고 보고서에 오류로 기록하십시오. 명백한 오식(obvious misprint)은 유일한 예외입니다(아래 참조).

• 증명이 필요해 보인다고 해서 논문 결과에 가설을 절대 추가하지 마십시오. 가설을 추가하면 결과가 약화됩니다. 명제 자체에 반례가 있을 때만 추가하고, 증명의 한 단계가 실패해서가 아닙니다. 그런 다음 이전 규칙을 따르십시오. 그렇지 않으면 수정된 논증으로 명제를 있는 그대로 증명하고, 증명의 공백을 E-항목(E-item)으로 기록하십시오. 증명과 반례를 모두 찾을 수 없는 경우, 누락된 부분을 사용자에게 알리십시오. 사용자는 계속 작업할지 아니면 편차로 문서화된 약한 명제를 형식화할지 결정합니다.

• 충실한 증명. 논문의 증명으로 각 결과를 증명하십시오: 동일한 중간 주장, 동일한 구성 및 사례 분할, 논문이 인용하는 동일한 이전 결과. 논문의 증명이 인용하는 결과가 그 *경로(route)*를 형성합니다. 형식적 증명은 동일한 경로를 가져야 하며, 경로 검사(Phase 6)가 이를 확인합니다. 기계적인 부분만 다를 수 있습니다: 전술(tactic), 일상적인 단계를 마무리하는 Mathlib 보조정리, 독립적인 단계의 순서, 논문의 한 단계를 패키징하는 도움말 보조정리. Mathlib에 번호가 매겨진 결과가 우연히 있더라도 논문의 논증으로 증명하십시오. 단, 논문 자체가 그 결과를 알려진 것으로 취급하는 경우(인용하거나 표준적이라고 부르는 경우)는 예외입니다.

• 반드시 필요한 경우에만 논문의 증명에서 이탈하십시오. 즉, 다음 이유 중 하나이고 다른 이유는 없어야 합니다:

  1. 해당 단계에서 논문의 논증이 틀렸거나 공백이 있으며, 논문의 선을 따라 수리할 수 없는 경우(해당 단계는 E-항목이기도 합니다);
  2. 해당 단계에 Lean에 없고 프로젝트가 합리적으로 구축할 수 없는 수학이 필요하며(도달할 수 없는 인용 결과의 경우처럼), 다른 논증이 이를 피하는 경우;
  3. 해당 단계가 형식화에서 반드시 사용해야 하는 표현(원칙 참조)에서 의미가 없어서 충실한 번역이 다른 논증이 되는 경우.

  더 짧고, 더 우아하고, 더 일반적이거나 더 자동화된 증명은 이유가 아닙니다. 형식화하기 더 쉽거나 더 빨리 구축할 수 있는 증명도 아닙니다. 발견한 더 간단한 논증은 여전히 보관할 가치가 있습니다: 보고서의 "다음 단계" 섹션(Phase 8)을 위해 개요와 함께 기록하고, 결과는 논문의 논증으로 증명하십시오. 이유가 요구하는 만큼만 이탈하십시오: 증명이 아니라 단계를 수리하십시오. 이탈이 번호가 매겨진 결과의 전체 논증을 대체해야 한다면(단순히 한 단계가 아니라), 이유와 함께 먼저 사용자에게 제안하십시오. 다른 작업은 그동안 계속됩니다.

• 모든 이탈을 항상 보고하십시오. 각 이탈에 대해 논문이 무엇을 하는지, 형식화가 대신 무엇을 하는지, 어떤 이유로 변경이 강제되었는지 기록하십시오. 선언문의 docstring("논문과의 이탈: …"), 보고서의 이탈 표, formalization.yaml(fidelity.divergences), 모든 동반 텍스트, 경로가 변경될 때 경로 검사의 기록된 차이점 파일, 그리고 다음 상태 보고서에 기록하십시오. 이 중 하나라도 누락된 이탈은 결함입니다: 조용히 변경된 명제를 찾고 수정하는 것처럼 찾아서 수정하십시오.

• 도달할 수 없는 인용 결과. 인용된 결과에 아직 어떤 Lean 라이브러리에도 없는 수학이 필요할 수 있습니다. 해당 수학을 프로젝트에서 구축하는 것이 적당한 노력이라면 구축하십시오. 그렇지 않으면 기본값은 조건부 형식화입니다: 해당 결과는 증명에서 사용하는 모든 명제의 명명된 가설이 됩니다. 묻지 않고 기본값을 적용하고, 다음 상태 보고서에 보고하십시오. 누락된 수학을 구축하는 것이 크지만 실행 가능한 노력일 때만 사용자에게 물으십시오: 그 노력을 들일지 여부는 사용자의 결정입니다. 그동안 기본값 아래에서 다른 작업을 계속하십시오. 사용자가 구축하기로 선택하면 작업을 계층(layer)으로 계획하십시오. 각 계층은 일부 가설을 더 기본적인 가설로부터의 구성과 증명으로 대체하고, 릴리스 가능한 상태로 끝납니다. 이러한 가설만 반례 없이 논문 결과에 추가될 수 있습니다. 조건부 형식화를 완전한 것으로 절대 제시하지 마십시오: README, formalization.yaml 및 보고서는 조건부임을 명시하고 가정하는 항목을 나열합니다.

• 명제의 실수. 명제가 명백한 오식(잘못된 인덱스, 이름이 바뀐 경우, - 1 누락)으로만 거짓이고, 의도된 읽기가 하나뿐인 경우, 해당 읽기를 즉시 라이브러리와 Challenge에 형식화하십시오. 각 수정 사항을 보고서와 사용자에게 보내는 다음 상태 보고서에 나열하십시오. 둘 이상의 수정이 가능한 경우, 명제를 거짓으로 취급하십시오.

• 거짓 도움말 보조정리(사용자나 초안이 도입한 것)는 가능할 때 Lean(decide, norm_num 또는 #eval)에서 확인된 구체적인 반례가 필요합니다. 그런 다음 최소 가설을 추가하고, 호출자를 업데이트하고, 커밋 메시지에 변경 사항을 기록하십시오.

• 끝에는 sorry(Challenge.lean 외부), admit, axiom, native_decide 또는 implemented_by가 없습니다. native_decide는 공리를 추가하며, Comparator가 이를 거부합니다.

• Mathlib 이름이나 시그니처를 절대 추측하지 마십시오. .lake/packages/mathlib에 고정된 소스를 grep하거나 #check, exact? 및 Loogle을 사용하십시오. Mathlib는 종종 선언의 이름을 바꾸고 폐기(deprecate)하며, 폐기 경고는 대체 이름을 알려줍니다.

• 컴파일할 수 없는 경우(도구 체인이 없거나 사용자가 금지하는 경우), Lean을 컴파일하지 않고 작성하십시오. 모든 이름, 시그니처 및 가져오기 경로를 고정된 Mathlib 소스와 대조하고, 명제 우선 순서를 유지하며, 각 결과를 검증되지 않은 것으로 레이블하십시오. 나중에 프로젝트를 컴파일하는 사람은 Phase 3부터 시작합니다.

• 체크아웃당 한 번에 하나의 lake build를 실행하십시오. 동시에 실행되는 빌드는 서로의 .olean 파일을 삭제하며, 프로젝트에서 열린 편집기는 자체 lake setup-file 빌드를 실행합니다. "object file … does not exist"가 표시되면 편집으로 우회하지 말고 다시 시도하십시오.

• 다른 사람이 볼 수 있는 작업을 수행하기 전에 물으십시오: 푸시, 저장소 생성, 저장소 공개 설정 변경, 풀 리퀘스트 열기/닫기, 브랜치 삭제, Palomar의 사전 점검 실행, Palomar에 제출, 등록. 이 중 하나에 대한 허가가 다른 것에 대한 허가는 아닙니다.

• 저자는 사람입니다. AI 시스템은 README, CREDITS.md 및 formalization.yaml의 automation 섹션에서 신용하되, 저자나 관리자로 절대 표시하지 마십시오.

• 처음부터 실행 로그를 유지하십시오("실행 로그" 참조). 이를 CREDITS.md, formalization.yaml 및 상태 보고서에 보고하십시오.

워크플로우

단계	목표	완료 조건
0. 설정	작업 기록, 미결 질문하기	설정이 기록됨
1. 목록 작성	논문 파악: 결과, 정의, 상수, 인용 및 증명 출처, 의심되는 오타	작업 체크리스트 완료
2. 프로젝트	Mathlib 릴리스 기반 Lean 프로젝트, 모듈 시스템 사용, 논문 섹션별 배치	lake build 실행
3. 명제	모든 정의와 번호가 매겨진 결과를 sorry 증명으로 서술; Challenge	명제가 자세히 서술되고 논문에 대한 독립적 검토 통과; 기준선 커밋
4. 1단계	논문이 증명하는 모든 것을 논문의 증명으로 증명	인용된 결과만 External/에 공리로 남음; 모든 이탈 보고됨
5. 2단계	인용된 결과 증명	공리 0개; 여전히 가정된 모든 결과는 명명된 가설
6. 검증	공리 감사, 의존성 테이블, 경로 검사, 솔루션 및 Comparator	scripts/Audit.lean 및 경로 검사 통과; 증명을 논문과 비교; Comparator 승인
7. 정리	경고 없음, 미사용 가설 없음, 오해의 소지가 있는 이름 없음, 경로 변경 없음	빌드에 Challenge의 sorry만 표시됨; 경로 검사 여전히 통과
8. 감사	REPORT.md, README.md, CREDITS.md; 비공개 NEXT.md	모든 발견 사항을 TeX 소스와 대조 확인; 모든 후속 후보를 참신성 및 기준과 대조 확인
9. 패키징	CI, Palomar 파일 및 검사; 허가를 받아 게시 및 사전 점검	Palomar의 로컬 검사 통과; 게시 후 사전 점검에서 status: pass 보고

각 이정표에서 커밋하고, 변경 사항과 이유를 설명하는 메시지를 포함하십시오.

0단계: 설정

다음을 기록하십시오. 스스로 해결할 수 없는 것에 대해서만 사용자에게 물으십시오:

paper:            arXiv ID와 버전(또는 DOI); 가능하면 소스 TeX; 이후 버전