Pristatome: Milenijaus prizo uždavinio „Yang-Mills masės tarpas“ formalus įrodymas Coq aplinkoje
shariq81·▲ 2·21.02.2026 22:40
Santrauka lietuviškai
Nepriklausomas tyrinėtojas kartu su neuro-simbolinio dirbtinio intelekto programa kelis mėnesius formaliai įrodė Milenijaus prizo „Yang-Mills masės tarpas“ uždavinį Coq teoremų įrodinėtojo aplinkoje. Baigtinės gardelės topologija buvo visiškai susieta su ℝ⁴ kontinuumu rekonstruojant 5 Osterwalder-Schrader aksiomas, o Milenijaus formuluotė išskaidyta į 657 nuoseklius Qed įrodymus. Visas metodologinis pagrindas remiasi tik 4 standartinėmis vadovėlių aksiomomis, o rezultatai atvirai paskelbti Zenodo platformoje.
Originalus pavadinimas
Show HN: Formally Verified a Millennium Prize Problem in Coq Yang-Mills Mass Gap
Susijusios naujienos