ما یک اثبات کننده قضیه عصبی برای ناب که حل انواع مشکلات چالش برانگیز المپیاد دبیرستانی، از جمله مسائل از AMC12 و AIME مسابقات، و همچنین دو مشکل اقتباس شده از IMO.^[1] Prover از یک مدل زبان برای یافتن شواهدی برای اظهارات رسمی استفاده می کند. هر یک