Vi beskriver ett bevis på Central Limit Theorem som har verifierats formellt i Isabelle bevis assistent. Vår formalisering bygger vidare på och utökar Isabelles bibliotek för analys och mått-teoretisk sannolikhet. Beviset på teoremet använder karakteristiska funktioner, som är ett slags Fourier transform, för att visa att, under lämpliga hypoteser, summor av slumpmässiga variabler konvergerar svagt till den normala standardfördelningen. Vi diskuterar också biblioteken och infrastrukturen som stödde formaliseringen, och reflekterar över några av de lärdomar vi har lärt oss av arbetet.
REF slutförde nyligen ett bevis på den centrala gränssatsen, som är den princip som ligger till grund för koncentrationsgränserna.
A Formally Verified Proof of the Central Limit Theorem
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Computer Science', 'Mathematics']}