عن المشروع

Descent هو مشروع برمجي مكتوب بلغة Lean 4 يوفر إطارًا رياضيًا رسميًا لنظرية الجينات. يركز بشكل أساسي على قابلية نقل الدرجات الجينية المتعددة (PGS)، ويتناول ثلاث أسئلة أساسية تتعلق بدقتها وقيودها عبر مختلف السكان. يحتوي المستودع على براهين صارمة تم تطويرها في ملف OpenQuestions.lean تصنف معلومات الخسارة الفردية والضوضاء. تُثبت هذه البراهين نطاقات قابلة للتحقيق بدقة عند لحظات ثانية ثابتة ومدخلات جينية، وتصف الإغلاق التطوري أو الإبلاغ المحدود، وتحدد عكسات الترتيب المترتي والتكلفة القرار. تشمل المجالات النظرية خسارة قابلة للتكامل مربعًا عشوائية لنظرية المعلومات وفئات نموذجية صريحة محدودة للنطاقات الدقيقة. بالإضافة إلى ذلك، يتم استخراج ضوضاء الخسارة الغاوسية من قياس غاوسي. يتم توفير تدقيق مركب للأكسيمات في ملف CheckThreeQuestions.lean. للحصول على نتائج مفصلة وحدود تتعلق بتوقع الدقة الديمغرافية للدرجات الجينية المتعددة، يُوجه المستخدمون إلى وثيقة UNIVERSAL_PORTABILITY.md. البناء لبناء المشروع، شغّل الأوامر التالية: lake exe cache get lake build Descent ValidationShared المساهمة مرحبًا بالمساهمات. ومع ذلك، تنطبق مواصفات صارمة: - لا يُسمح أبدًا باستخدام المحاكاة لتكييف النماذج؛ فهي تُستخدم حصرًا لتحقق الاستنتاجات القائمة. - يُسمح فقط بثلاثة أكسيومات: propext، Classical.choice، وQuot.sound. الرخصة المشروع مرخص تحت رخصة Apache-2.0.