أداة مفهومية لتحقق من التقديرات التقريبية أثار هذا الموضوع بعض المناقشات الحديثة مع بيوورن برингمان. تعد البرمجيات الرياضية الرمزية متقدمة ومتطورة في العديد من المهام الرياضية مثل الجبر وحساب التفاضل والتكامل والتحليل العددي. ومع ذلك، ليس لدينا أدوات مشابهة ومتطورة للتحقق من التقديرات التقريبية - وهي متراجحات تفترض صحتها لparameters كبيرة بشكل تعسفي، مع خسائر ثابتة. في هذا السياق، تعتبر التقديرات الوظيفية مهمة للغاية، حيث تتضمن parameters دالة أو تسلسل غير معروف (موجود في مساحة دالة مناسبة مثل المساحة ). ولكن لهذه المناقشة، سأركز على الوضع البسيط الذي envolves تقديرات تقريبية تتعلق بعدد محدود من الأعداد الحقيقية الموجبة، والتي يتم دمجها باستخدام العمليات الحسابية مثل الجمع والضرب والقسمة والأس والحد الأدنى والأقصى (ولكن ليس الطرح). مثال معتاد على مثل هذه المتراجحة هو المتراجحة الضعيفة بين الوسط الحسابي والوسط الهندسي: [ \left(abc\right)^{1/3} \leq C \max(a, b, c) ] حيث ( a, b, c ) هي أعداد حقيقية موجبة، و ( C ) هو ثابت غير محدد. بمبادئ فكرية بسيطة، يمكن تبسيط هذه المتراجحة إلى حالة محددة. على سبيل المثال، لنفترض أن ( \max(a, b, c) = a ). في هذه الحالة، يجب إثبات أن: [ \left(\frac{b}{a}\right)^{1/3} \left(\frac{c}{a}\right)^{1/3} \leq C ] وهو ما يمكن إثباته باستخدام البرمجة الخطية، حيث يمكن للبرامج الحاسوبية تحديد مزيج خطي من الفرضيات المقدمة. تطبيق عملي قدت هذه الأداة في أحد أبحاثي القديمة، حيث كنت أرغب في إثبات التقدير التالي: [ \max(x_1, x_2, x_3) + \min(y_1, y_2, y_3) \leq C (\text{median}(x_1, x_2, x_3) + \text{median}(y_1, y_2, y_3)) ] لأي ( x_1, x_2, x_3 ) و ( y_1, y_2, y_3 ) التي تحقق الشروط: [ \max(x_1, x_2, x_3) \leq \alpha ] [ \text{median}(x_1, x_2, x_3) \leq \beta ] [ \min(x_1, x_2, x_3) \leq \gamma ] [ \max(y_1, y_2, y_3) \leq \delta ] [ \text{median}(y_1, y_2, y_3) \leq \epsilon ] [ \min(y_1, y_2, y_3) \leq \zeta ] حيث ( \alpha, \beta, \gamma, \delta, \epsilon, \zeta ) هي أعداد حقيقية موجبة. تمكنت من إثبات هذا التقدير في ثلاث أو أربع خطوات من المتراجحات البسيطة، ولكن كان علي إجراء عشراة المزيد من المتراجحات من هذا النوع، وهو ما جعل المهمة مرهقة وملائمة للآليات. تطوير الأداة في الآونة الأخيرة، زادت كمية البرمجة التي أقوم بها (باستخدام Python بشكل رئيسي)، بمساعدة كبيرة من نماذج اللغات الكبيرة في توليد عينات رمزية أولية للمهام المختلفة أو إكمال الرمز جزئياً. قررت تحدي نفسي بمهمة أكثر تعقيداً، وهي تطوير أداة لتحقق من المتراجحات من النوع المذكور. بعد حوالي أربع ساعات من البرمجة، وبمساعدة مستمرة من نموذج لغة كبير، تمكنت من إنشاء أداة مفهومية لهذا الغرض، ويمكن العثور على الكود في هذا المستودع على GitHub. مثال على استخدام الأداة للتحقق من المتراجحة الأولى (1)، يتم استخدام الكود التالي في Python: python a = Variable("a") b = Variable("b") c = Variable("c") assumptions = Assumptions() assumptions.can_bound((a * b * c) ** (1 / 3), max(a, b, c)) والإخراج (الذي يبدو مطولاً قليلاً) يؤكد صحة المتراجحة: Checking if we can bound (((a * b) * c) ** 0.3333333333333333) by max(a, b, c) from the given axioms. We will split into the following cases: [[b <~ a, c <~ a], [a <~ b, c <~ b], [a <~ c, b <~ c]] Trying case: ([b <~ a, c <~ a],) Simplify to proving (((a ** 0.6666666666666667) * (b ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : b <~ a raised to power 0.33333333 c <~ a raised to power 0.33333333 Trying case: ([a <~ b, c <~ b],) Simplify to proving (((b ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : a <~ b raised to power 0.33333333 c <~ b raised to power 0.33333333 Trying case: ([a <~ c, b <~ c],) Simplify to proving (((c ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (b ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : a <~ c raised to power 0.33333333 b <~ c raised to power 0.33333333 Bound was proven true in all cases! بالطبع، هذا البرهان غير أنيق للغاية، ولكن الأناقة ليست هي الهدف هنا؛ الهدف هو الآليات. يمكن لهذا الكود التعامل مع تقديرات أكثر تعقيداً مثل (3)، ولكنه حالياً لا يتعامل بشكل فعال مع الفرضيات التي تتضمن تعبيرات معقدة مثل ( \log ) أو ( \sqrt{\cdot} ). آفاق التطوير المستقبلي هذه الأداة هي مجرد مفهوم أولي، ولكنها تثبت إمكانية إنشاء أداة أكثر تطوراً لتنفيذ مهام متقدمة. أحد الأمثلة على هذه المهام هو التحقق الآلي من ادعاء مثل: [ \sum_{i=1}^n \frac{a_i}{\sqrt{i}} \leq C \left( \sum_{i=1}^n a_i \right)^{1/2} ] للأعداد الحقيقية الموجبة ( a_i ). مثال آخر هو التحقق الآلي من تقديرات تعبيرات متعددة الخطوط لدوال مختلفة، بناءً على مقاييس هذه الدوال في مساحات دالة قياسية مثل مساحات Sobolev، وهذا هو مهمة شائعة في نظرية المعادلات التفاضلية الجزئية والتحليل التوافقي. كما أشارت بيوورن برингمان في مقالة حديثة لها، يمكن أن تغير أدوات التحقق الآلي طريقة كتابة البراهين. قد يكون هناك دور للذكاء الاصطناعي في هذا السياق، مثل اقتراح تقسيمات محتملة لمجموعات أو تكاملات مختلفة، ولكن هذا سيكون هدفاً بعيد المدى. التعاون والتطوير من الأفضل أن يتم تطوير هذا النوع من البرمجيات كمشروع تعاوني يجمع بين الرياضيين والمبرمجين المحترفين. أنا مهتم باستقبال النصائح حول كيفية المضي قدماً في مثل هذا المشروع (مثل هل من المنطقي دمج مثل هذه الأداة في منصة موجودة مثل SageMath)، وما هي الخصائص الأكثر رغبة في أداة عامة للتحقق من التقديرات. من رغباتي هو القدرة على إعطاء الأداة تعبيراً للتقدير (مثل تكامل متعدد الخطوط لدوال غير معروفة)، بالإضافة إلى مجموعة ثابتة من الأدوات لتقدير هذا التكامل (مثل تقسيم التكامل إلى قطع، التكامل بالأجزاء، استخدام متراجحات Hölder و Sobolev)، والاطلاع على أفضل تقدير يمكن للأداة إنتاجه (مع شهادة برهان مستقلة). يمكن أيضاً تخيل إمكانية إخراج هذه الشهادات في لغة مساعدة برهان رسمية مثل Lean. ولكن ربما تكون هناك خصائص أخرى مفيدة يمكن للقراء اقتراحها. الخلاصة هذه الأداة المفهومية تفتح الباب أمام تطوير أدوات أكثر تطوراً وفعالية لرياضيات التحليل والمعادلات التفاضلية الجزئية. التعاون بين الرياضيين والمبرمجين المحترفين يمكن أن يسهم في تحقيق هذا الهدف، مما يوفر حلولاً آلية لمهمات رياضية معقدة ومرهقة.