The set of primes is supernatural: a Lean formalization of the statement of the conjecture
تقدم هذه الورقة صياغة كاملة، ومحققة آلياً باستخدام لغة Lean 4، للتخمين القائل بأنه لا توجد دالة غير ثابتة مشتقة من دالة الهوية، والثوابت، وعمليات نقطية محدودة (الجمع، والضرب، والرفع إلى أس) ترسم كل عدد صحيح موجب إلى عدد أولي، مما يحول التخمين إلى هدف دقيق وقابل للتحقق بواسطة النواة لأنظمة الاستدلال الآلي.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل مكتبة شاسعة ولانهائية، حيث كل كتاب فيها هو عبارة عن رقم. في هذه المكتبة، توجد نادٍ حصري للغاية يسمى "الأعداد الأولية". هذه الأعداد هي أرقام لا يمكن بناؤها بضرب أرقام أصغر منها؛ إنها الذرات غير القابلة للتجزئة في الحساب، مثل 2، أو 3، أو 5، أو 7. لقرون مضت، حاول الرياضيون كتابة وصفة بسيطة واحدة — آلة مصنوعة من أدوات رياضية أساسية — يمكنها أن تخرج فقط أعضاء هذا النادي الخاص. أرادوا آلة، مهما كان الرقم الذي تغذيها به، فإنها ستنتج دائمًا عددًا أوليًا.
الأدوات المسموح بها في هذه الوصفة هي أكثر الأدوات أساسية التي نعرفها: جمع الأرقام معًا، وضربها، ورفعها إلى قوى (مثل التربيع أو التكعيب). يمكنك خلط ومطابقة هذه الأدوات كما تشاء، لكن لا يمكنك استخدام أشياء معقدة مثل القسمة أو الجذور التربيعية. السؤال الكبير هو: هل هناك طريقة لبناء آلة باستخدام هذه الأدوات البسيطة فقط لا تخطئ أبدًا؟ هل يمكن لمثل هذه الآلة أن تولد قائمة لا تنتهي من الأعداد الأولية، أم أنها ستتعثر في النهاية وتنتج رقمًا ليس أوليًا؟ هذا ليس مجرد لعب؛ إنه يمس جوهر كيفية هيكلة الأرقام. إذا وجدت مثل هذه الآلة، فهذا يعني أن الأعداد الأولية تتبع نمطًا بسيطًا وقابلًا للتنبؤ. وإذا لم توجد، فهذا يعني أن الأعداد الأولية برية، وفوضوية، و"خارقة للطبيعة" بطريقة تتحدى الصيغ البسيطة.
هذه الورقة هي قصة تحقيق رقمية حول هذا السؤال تحديدًا. لقد قام المؤلف، أرنو مايو، بأخذ ورقة بحثية رياضية محددة اقترحت تخمينًا جريئًا (فرضية)، وترجمت الورقة بأكملها إلى لغة حاسوبية تسمى "Lean". فكر في "Lean" كحكم صارم للغاية يتحقق من كل خطوة في البرهان الرياضي لضمان أنها سليمة منطقيًا بنسبة 100%، دون أي مجال للخطأ البشري أو لحظات "أعتقد أن هذا يعمل". الورقة لا تحل لغز ما إذا كانت آلة توليد الأعداد الأولية موجودة، بل تبني نموذجًا رقميًا مثاليًا وغير قابل للكسر لقواعد اللعبة.
النتيجة الرئيسية لهذا العمل هي أن النظرية الكاملة وراء تخمين "آلة الأعداد الأولية" قد تمت برمجتها بنجاح داخل الحاسوب. كل تعريف، وكل مثال، وكل جدول أرقام من الورقة الأصلية يعيش الآن داخل هذا الملف الرقمي. قام المؤلف بالتحقق من 89 مثالًا مختلفًا لهذه "الدوال الطبيعية" (الاسم الفخم للآلات المبنية من الجمع والضرب والقوى). ولكل منها، حسب الحاسوب النتائج وأكد أن جميعها تفشل في النهاية في إنتاج عدد أولي. على سبيل المثال، عملت إحدى الدوال بشكل مثالي لأول ستة أرقام ولكنها تعطلت عند الرقم السابع. أثبت الحاسوب حالات الفشل هذه بيقين مطلق، باستخدام شهادات رقمية متقدمة للتحقق من أرقام ضخمة قد يستغرق البشر سنوات للتحقق منها يدويًا.
ومع ذلك، فإن الورقة واضحة جدًا بشأن ما لم تفعله. إنها لم تثبت أن آلة الأعداد الأولية مستحيلة. لم تجد الإجابة النهائية. التخمين المركزي — وهو أنه لا توجد مثل هذه الآلة — لا يزال مشكلة مفتوحة، "مشكلة مفتوحة مسماة" في الكود الحاسوبي، تنتظر إنسانًا أو ذكاءً اصطناعيًا ليثبتها أخيرًا. تقول الورقة أساسًا: "إليك كتاب القواعد الدقيق، وإليك الدليل على أن كل آلة جربناها حتى الآن قد فشلت، لكن الحكم النهائي لم يصدر بعد".
قام المؤلف أيضًا بتوسيع اللعبة قليلًا. تساءل: "ماذا لو أضفنا بعض الأدوات الإضافية، مثل المضروب (factorial) (ضرب الرقم في جميع الأرقام التي دونه) أو أسهم كونوت (طريقة لكتابة قوى ضخمة)؟" وبنى فئة جديدة وأكبر من الآلات باستخدام هذه الأدوات الإضافية، وصاغ تخمينًا جديدًا، وأكثر صعوبة، مفاده: أنه حتى مع هذه الأدوات الخارقة، لا يمكنك بناء آلة تصنع أعدادًا أولية فقط. هذا التخمين الجديد أيضًا ظل مفتوحًا، غير مثبت، ولكنه مكتوب الآن بطريقة يمكن للحاسوب التحقق منها إذا توصل شخص ما للبرهان في النهاية.
باختصار، هذه الورقة هي عمل ضخم من أعمال الترجمة والتحقق. إنها تأخذ فكرة رياضية معقدة حول الطبيعة الفوضوية للأعداد الأولية وتحبسها في خزنة رقمية حيث يتم التحقق من كل قاعدة بواسطة آلة. إنها تؤكد أنه لكل مثال محدد تم اختباره، تفشل "آلة الأعداد الأولية"، لكنها تترك السؤال النهائي حول ما إذا كان وجود مثل هذه الآلة ممكنًا من الناحية النظرية كتحدٍ للمستقبل. يبدو أن الأعداد الأولية "خارقة للطبيعة" حقًا، إذ تقاوم أي صيغة بسيطة نحاول حبسها بها.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.