يقدم الباحثون TreeThink، وهي مكتبة بايثون مفتوحة المصدر مصممة للبحث الشجري المعدني وغير المتزامن بالكامل في إثبات النظريات العصبية. تدمج طرق البحث الراسخة مع خطوط أنابيب الاستدلال القائمة على vLLM وتقنيات تقييم العقد المتنوعة.
- يدعم Lean~4 وRocq وIsabelle/HOL والاستدعاء باللغة الطبيعية.
- يتصل مباشرة بخادم REPL لكل لغة للتحقق في الوقت الفعلي واستخراج حالة البرهان.
- يُظهر تسريعًا في الوقت الفعلي يصل إلى 6.3x من التنفيذ غير المتزامن على معايير miniF2F وMATH500.
تتيح المكتبة البحث عن البراهين الرسمية عبر اللغات ودعم الاستدعاء باللغة الطبيعية، مع نشر الكود المصدري بموجب رخصة MIT.