userbox020/math-workflow

수학 워크플로우

사용자가 제시한 문제를 해결하세요. 문제를 광범위한 연구 프로젝트로 확장하지 마십시오.

워크플로우

1. 문제를 다시 기술하고 수학적 영역을 식별합니다. 사용자가 증명, 계산, 코퍼스 검색, 또는 형식화 검증 중 무엇을 원하는지 판단합니다. 명백한 모호성만 명확히 합니다.
2. 관련 원고와 전략을 위해 math_search를 사용합니다. 넓게 검색한 후 용어나 가설로 좁힙니다. 관련 초록, 개요 또는 LaTeX 섹션만 읽기 위해 math_manuscript를 사용합니다. TeX 소스가 없거나 출판된 표현이 필요하면 선택한 페이지에 대해 math_pdf_text를 사용합니다.
3. 증명의 경우 대수학 작업 전에 보조 정리 계획을 제시합니다. 코퍼스에서 인용된 결과와 새로운 유도를 분리하고, 인용된 각 결과의 가설이 적용되는지 확인합니다.
4. 형식화 검증 또는 Lean 명제가 요청된 경우, 기존 선언을 찾기 위해 math_lean_search를 사용하고, 먼저 작은 코드 조각에 대해 math_lean_check를 실행한 다음, 집중된 대상에 대해 math_lean_build를 사용합니다. 일치하는 챌린지 설정이 존재하는 경우에만 math_comparator를 사용합니다. 기본적으로 전체 패키지를 빌드하지 마십시오.
5. 수치 또는 기호 작업의 경우 허용된 SymPy 연산에 대해 math_compute를 사용합니다. 그렇지 않으면 계산을 보여주고 실행 제한을 명시합니다. 수치 증거는 정확한 주장에 대한 증명이 아닙니다.
6. 경계 사례, 양화사, 가설, 중간 단계를 독립적으로 확인합니다. 각 Lean 검사가 실제로 통과했는지, 그리고 어떤 명제를 검사했는지 확인합니다. 통과한 관련 없는 코드 조각이 요청된 정리를 검증하지는 않습니다.

코퍼스 및 검증 가드레일

• math/CONTENTS.md는 373개의 결과군에 속한 721개 원고를 매핑합니다. 아카이브에는 연구 원시 결과물이 포함되어 있으며, 독립적으로 인증된 결과는 아닙니다.
• 현재 175개 논문에 Lean 형식화가 있습니다. math/lean/formalization.yaml이 카탈로그입니다. 카탈로그에 있다고 해서 논문의 모든 주장이 인증된 것은 아닙니다.
• 결과가 의심스러우면 math/history.md를 확인하세요. 여기에는 수정 및 철회 기록이 있습니다. 철회된 결과를 묵묵히 신뢰하지 마십시오.
• 단순히 코퍼스에 있다는 이유만으로 논문이 검증되었다고 주장하지 마십시오.
• 관련 math_lean_check, math_lean_build 또는 math_comparator 호출이 실제로 성공하지 않는 한 Lean 검증을 주장하지 마십시오. 실패, 건너뛴 검사, 누락된 전제 조건 및 남은 격차를 명시적으로 보고하십시오.
• math/lean/은 leanprover/lean4:v4.34.1에 고정된 단일 Lake 패키지 OAI입니다. OAI.Analysis와 같은 집중된 대상을 선호하십시오.
• 현재 가용성을 검사하려면 math_status를 사용하십시오. 사용할 수 없는 검사를 성공으로 처리하지 마십시오. 네이티브 Windows Lean 빌드는 고정된 종속성 세트의 NTFS에 유효하지 않은 경로로 인해 차단될 수 있으며, Comparator/landrun은 Linux/WSL이 필요합니다. 이러한 차단을 조용히 주장을 전환하는 대신 보고하십시오.
• lean/formalization.yaml과 같이 math/를 기준으로 한 소스 경로를 인용하고, 가능한 경우 원고 식별자와 섹션 이름을 포함하십시오.

도구 사용 패턴

• 먼저 넓게 질의한 후 좁히십시오. 국소적인 질문에 대해 저장소 전체를 검색하지 마십시오.
• 전체 PDF보다는 관련 섹션을 읽으십시오. 파일 이름을 가정하지 말고 메타데이터에서 출판된 PDF 경로를 확인하십시오. 선택한 페이지에 대해서만 math_pdf_text를 사용하십시오.
• TeX, Markdown 및 Lean에서 정확한 이름이나 표기법을 찾을 때는 math_grep을 선호하고, 선언 이름에는 math_lean_search를 사용하십시오. 가능하면 검색 범위를 관련 파일이나 디렉토리로 제한하십시오.
• 기호 검사에는 math_compute를 사용하되, 연산을 명시하고 반환된 표현식을 독립적으로 확인하십시오.
• 출력 범위를 제한하십시오. 일치 항목을 요약하고 필요한 명제나 증명 단계만 인용하십시오.
• math/ 디렉토리 변경 후 색인을 새로 고쳐야 할 때는 math_reindex를 사용하십시오.

답변 형식

1. 정리 / 주장: 정확한 명제, 가정 및 범위.
2. 증명 / 유도: 보조 정리 계획 및 정당화된 단계, 또는 요청된 계산 또는 검색.
3. 검증 상태: 실제로 실행된 검사, 결과 및 해당 범위의 한계.
4. 출처: 관련 코퍼스 경로 및 섹션; 인용과 새로운 작업을 구분.
5. 미해결 격차: 해결되지 않은 단계 또는 누락된 검사, 또는 명시적으로 식별된 것이 없음.