رغم النجاح الكبير الذي حققته النماذج اللغوية الكبيرة (LLMs)، تظل مهمة إثبات النظريات واحدة من أصعب مهام الاستدلال، والتي لا تزال بعيدة عن الحل الكامل. وقد أظهرت الطرق السابقة التي تعتمد على النماذج اللغوية نتائج واعدة، لكنها لا تزال تعاني من صعوبة إثبات نظريات حتى على مستوى المدرسة الثانوية. إحدى القيود الشائعة لهذه الطرق هي افتراضها وجود مكتبة نظرية ثابتة طوال عملية إثبات النظريات بأكملها. ومع ذلك، كما نعلم جميعًا، فإن إنشاء نظريات جديدة أو حتى نظريات مفيدة ليس فقط مفيدًا، بل ضروريًا ومهمًا جدًا لدفع عجلة التقدم في الرياضيات وإثبات نتائج أكثر تعقيدًا وعمقًا. في هذا العمل، نقدم LEGO-Prover، الذي يستخدم مكتبة مهارات متزايدة تحتوي على نظريات ونتائج فرعية مُثبتة كمهارات لتعزيز قدرات النماذج اللغوية الكبيرة المستخدمة في إثبات النظريات. من خلال بناء الإثبات بطريقة تطورية (Modular)، يمكّن LEGO-Prover النماذج اللغوية من استخدام المهارات الموجودة مسبقًا المستخرجة من المكتبة، وإنشاء مهارات جديدة أثناء عملية الإثبات. وتُطوّر هذه المهارات لاحقًا (باستخدام توجيه نموذج لغوي) لزيادة تنوّع المكتبة على مستوى أعمق. وتُضاف باستمرار مهارات قابلة لإعادة الاستخدام ومتعددة الوظائف إلى المكتبة، مما يمكّن من مواجهة مسائل رياضية متزايدة التعقيد. علاوةً على ذلك، تساعد المكتبة المُكتسبة في تقليل الفجوة بين الإثباتات البشرية والإثباتات الرسمية من خلال تسهيل استنتاج الخطوات المفقودة. وقد ساهم LEGO-Prover في تحسين معدل النجاح في مجموعة بيانات miniF2F-valid (من 48.0% إلى 57.0%) وفي مجموعة miniF2F-test (من 45.5% إلى 47.1%). خلال عملية الإثبات، تمكّن LEGO-Prover من إنشاء أكثر من 20,000 مهارة (نظريات/نتائج فرعية) وإضافتها إلى المكتبة المتزايدة. وتشير دراسة التحليل التجريبي (Ablation Study) إلى أن هذه المهارات الجديدة تُعد فعالة حقًا في إثبات النظريات، حيث ساهمت في تحسين معدل النجاح من 47.1% إلى 50.4%. كما نُشر الكود المصدري وجميع المهارات المُولَّدة.