إن ترسيخ الأدلة الرياضية الحالية يُعد عملية معروفة بصعوبتها البالغة. وعلى الرغم من عقود من البحث المتعلق بالأتمتة ومساعِدات البرهان، تظل كتابة الأدلة الرسمية عملية متعبة، ومتاحة فقط لعدد قليل من الخبراء. في حين ركزت الدراسات السابقة لتحسين الأتمتة على خوارزميات بحث قوية، لم تُبذل أي محاولات للاستفادة من الأدلة غير الرسمية المتاحة. في هذا العمل، نقدم طريقة تُسمى "رسم المخطط، وتحديثه، وبرهانه" (DSP)، التي تقوم بتحويل الأدلة غير الرسمية إلى مخططات برهان رسمية، ثم تستخدم هذه المخططات لتوجيه مُثبت آلي من خلال توجيه بحثه نحو مسائل فرعية أسهل. نستعرض حالتين مهمتين، حيث تُكتب الأدلة غير الرسمية إما بواسطة البشر أو تُولَّد بواسطة نموذج لغوي. تُظهر تجاربنا ودراسات التحليل التجريبي أن النماذج الكبيرة للغة قادرة على إنتاج مخططات رسمية جيدة التركيب، تتبع نفس خطوات الاستدلال الموجودة في الأدلة غير الرسمية. وتؤدي عملية توجيه مُثبت آلي باستخدام هذه المخططات إلى تحسين أداءه من 20.9% إلى 39.3% على مجموعة من مشكلات المسابقات الرياضية.