descent

Descent는 유전 이론을 위한 형식적 수학 프레임워크를 제공하는 Lean 4로 작성된 소프트웨어 프로젝트입니다. 주된 초점은 다유전자 점수(Polygenic Scores, PGS)의 이식성에 있으며, 서로 다른 집단에서의 정확성과 한계에 관한 세 가지 핵심 질문을 다룹니다. 이 저장소에는 개인 손실 정보와 잡음을 분류하는 `OpenQuestions.lean`에서 개발된 엄밀한 증명이 포함되어 있습니다. 이 증명들은 고정된 2차 모멘트와 유전적 입력에서 예리한 도달 가능 범위를 확립하고, 유한한 진화적 또는 보고적 폐쇄성을 특성화하며, 거리 순서 및 결정 비용 대우를 정의합니다. 이론적 영역에는 정보 정리를 위한 임의의 제곱 적분 가능 손실과 예리한 범위를 위한 명시적 유한 모델 클래스가 포함됩니다. 또한 가우시안 손실 잡음은 가우시안 측도에서 유도됩니다. 결합된 공리 감사는 `CheckThreeQuestions.lean`에 제공됩니다. 다유전자 점수 정확도의 인구통계학적 예측에 관한 자세한 결과와 한계는 `UNIVERSAL_PORTABILITY.md` 문서를 참조하십시오. ### 빌드 프로젝트를 빌드하려면 다음 명령을 실행하십시오: ```sh lake exe cache get lake build Descent ValidationShared ``` ### 기여 기여를 환영합니다. 그러나 엄격한 사양이 적용됩니다: - 시뮬레이션은 모델을 피팅하는 데 절대 사용되어서는 안 되며, 기존 도출을 검증하는 용도로만 사용됩니다. - 세 가지 공리만 허용됩니다: `propext`, `Classical.choice`, `Quot.sound`. ### 라이선스 이 프로젝트는 Apache-2.0에 따라 라이선스가 부여됩니다.