अपोलो एक स्वचालित प्रमेय सिद्धि प्रणाली है जो गणितीय प्रमेयों को सिद्ध करने के लिए लीन कंपाइलर और एलएलएम की तर्क शक्ति का संयोजन करती है। जहाँ पारंपरिक एलएलएम-आधारित प्रमेय सिद्धि विधियाँ ऐसे प्रमाण उत्पन्न करती हैं जो सत्यापन प्रणालियों द्वारा असंख्य (हज़ारों) प्रतिचयनों से होकर गुजरते हैं, वहीं अपोलो एक मॉड्यूलर पाइपलाइन का उपयोग करता है जिसमें एलएलएम प्रमाण उत्पन्न करता है, एजेंट प्रमाणों में वाक्यगत त्रुटियों को ठीक करते हैं, लीन त्रुटियों की पहचान करता है, असफल उप-प्रमेयों को अलग करता है, एक स्वचालित सॉल्वर का उपयोग करता है, और शेष उद्देश्यों के लिए कम खर्च में एलएलएम का उपयोग करता है। सुधारे गए उप-प्रमाणों के पुनर्संयोजन और पुनर्सत्यापन की यह प्रक्रिया उपयोगकर्ता द्वारा नियंत्रित अधिकतम प्रयासों तक दोहराई जाती है। मिनीएफ2एफ बेंचमार्क पर, यह 8B से कम प्राचलों वाले मॉडलों में 84.9% सटीकता प्राप्त करता है, जबकि प्रतिचयन लागत 100 से कम बनाए रखता है। इसके अलावा, यह गोएडेलप्रोवरएसएफटी की सटीकता को 65.6% तक सुधारता है और प्रतिदर्श जटिलता को 25,600 से घटाकर कई सौ कर देता है।
