چارچوبی با مشارکت پژوهشگر، خانواده‌ای از کدهای کوانتومی را کشف و اثبات‌پذیری آن را بررسی کرد

پژوهشی تازه در arXiv چارچوبی برای کشف ساختارهای ریاضی با کمک مدل‌های زبانی بزرگ پیشنهاد می‌کند که در آن تولید برنامه، ارزیابی دقیق، تعمیم ریاضی، بررسی گواهی‌شدهٔ ناممکن‌بودن و وارسی صوری اثبات، مراحل جداگانه‌اند. هدف این تفکیک آن است که اعتبار، تعمیم‌پذیری و بازتولیدپذیری هرکدام شواهد متناسب خود را داشته باشند.

پژوهشگران این روش را روی کدهای تصحیح خطای کوانتومیِ یاری‌شده با درهم‌تنیدگی (EAQECC) آزمودند. در مسئله‌هایی که از ابتدا فرمول یک خانوادهٔ کد را مشخص نمی‌کردند، برنامه‌های تکامل‌یافته ساخت‌هایی برای تعداد محدودی کیوبیت به دست دادند. پژوهشگران با بررسی این ساخت‌ها، آن‌ها را به خانوادهٔ $[[n,1,n-1;n-q-1]]_q$ تعمیم دادند: برای توان‌های اول $q\ge3$ و $n\ge2q+1$، و برای $q=2$ و مقادیر فرد $n\ge5$.

بر اساس چکیدهٔ پیش‌چاپ، Lean گواهی جبریِ زیربنای این خانواده را وارسی می‌کند. متن در دسترس در این منبع در میانهٔ جمله پایان می‌یابد؛ بنابراین جزئیات نتیجه‌های بعدی مقاله مشخص نیست.