Об этом проекте

Descent — это программный проект, написанный на Lean 4, который предоставляет формальную математическую основу для генетической теории. Его основное внимание сосредоточено на переносимости полигенных оценок (PGS), рассматривая три ключевых вопроса об их точности и ограничениях в разных популяциях. Репозиторий содержит строгие доказательства, разработанные в `OpenQuestions.lean`, которые классифицируют информацию об индивидуальных потерях и шум. Эти доказательства устанавливают точные достижимые диапазоны при фиксированных вторых моментах и генетических входных данных, характеризуют конечную эволюционную или отчётную замкнутость, а также определяют метрическое упорядочение и обратные утверждения о стоимости решений. Теоретические области включают произвольные квадратично интегрируемые потери для теорем об информации и явные классы конечных моделей для точных диапазонов. Кроме того, гауссов шум потерь выводится из гауссовой меры. Совместный аудит аксиом предоставлен в `CheckThreeQuestions.lean`. Для получения подробных результатов и ограничений, касающихся демографического прогнозирования точности полигенных оценок, пользователям следует обратиться к документации `UNIVERSAL_PORTABILITY.md`. ### Сборка Чтобы собрать проект, выполните следующие команды: ```sh lake exe cache get lake build Descent ValidationShared ``` ### Участие Вклад приветствуется. Однако применяются строгие требования: - Симуляции никогда не должны использоваться для подгонки моделей; они предназначены исключительно для проверки существующих выводов. - Разрешены только три аксиомы: `propext`, `Classical.choice` и `Quot.sound`. ### Лицензия Проект распространяется под лицензией Apache-2.0.