Nemotron-Math-Proofs-v1 عبارة عن مجموعة بيانات واسعة النطاق للاستدلال الرياضي والإثبات الرسمي تم إصدارها بواسطة NVIDIA في عام 2025، وهي مصممة لدعم تدريب وبحث نماذج اللغة الكبيرة في الاستدلال الرياضي المنظم وتوليد إثبات النظرية الرسمي Lean 4.

تحتوي هذه المجموعة من البيانات على ما يقارب 580,000 سؤال برهان رياضي باللغة الطبيعية، وما يقارب 550,000 عبارة رسمية مقابلة لنظريات Lean 4، وما يقارب 900,000 مسار استدلال مُولّد بواسطة النموذج، بالإضافة إلى شفرة برهان Lean 4 قابلة للتجميع. وهي مناسبة لتدريب وتقييم نماذج الاستدلال الرياضي الرسمي، وأنظمة الاستدلال طويلة السياق، وأساليب الاستدلال القائمة على التحقق.