Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
यह शोध पत्र Mechanic को प्रस्तुत करता है, जो एक नवीन एजेंट सिस्टम है जो एक औपचारिक प्रमाण (formal proof) के भीतर विफल उप-लक्ष्यों (subgoals) को अलग करने और उन्हें स्वतंत्र रूप से हल करने के लिए Lean के "sorry" प्लेसहोल्डर का उपयोग करता है, जिससे पूर्ण पुनरुत्पादन (full regeneration) की अक्षमताओं और पुनरावृत्ति सुधारों (iterative repairs) से जुड़े संदर्भ क्षरण (context degradation) से बचते हुए चुनौतीपूर्ण गणितीय बेंचमार्क पर स्वचालित प्रमेय प्रमाणन (automated theorem proving) में महत्वपूर्ण सुधार किया जा सके।