descent

Descent est un projet logiciel écrit en Lean 4 qui fournit un cadre mathématique formel pour la théorie génétique. Son objectif principal est la portabilité des scores polygéniques (PGS), en abordant trois questions centrales concernant leur précision et leurs limites dans différentes populations. Le dépôt contient des preuves rigoureuses développées dans `OpenQuestions.lean` qui classifient l'information de perte individuelle et le bruit. Ces preuves établissent des plages atteignables précises à seconds moments fixes et entrées génétiques, caractérisent une clôture évolutive ou de déclaration finie, et définissent les converses d'ordre métrique et de coût décisionnel. Les domaines théoriques incluent une perte arbitraire de carré intégrable pour les théorèmes d'information et des classes de modèles finis explicites pour les plages précises. De plus, le bruit de perte gaussien est dérivé de la mesure gaussienne. Un audit combiné des axiomes est fourni dans `CheckThreeQuestions.lean`. Pour des résultats détaillés et les limites concernant la prédiction démographique de la précision des scores polygéniques, les utilisateurs sont dirigés vers la documentation `UNIVERSAL_PORTABILITY.md`. ### Compilation Pour compiler le projet, exécutez les commandes suivantes : ```sh lake exe cache get lake build Descent ValidationShared ``` ### Contribution Les contributions sont les bienvenues. Cependant, des spécifications strictes s'appliquent : - Les simulations ne doivent jamais être utilisées pour ajuster des modèles ; elles servent exclusivement à valider des dérivations existantes. - Seuls trois axiomes sont autorisés : `propext`, `Classical.choice` et `Quot.sound`. ### Licence Le projet est sous licence Apache-2.0.