सेवा के बारे में
अनुवादितमैं एक औपचारिकीकरण इंजीनियर हूँ और शोध समूहों, पाठ्यपुस्तक लेखकों और टीमों के लिए Lean 4 में प्रमाण लिखता हूँ जिन्हें मशीन-चेक किए गए गारंटी की आवश्यकता होती है, न कि हाथ से किए गए तर्क। मुझे एक प्रमेय का कथन, एक पेपर या एक अस्पष्ट विनिर्देश दें - मैं इसे एक संकलन Lean प्रोजेक्ट में बदल देता हूँ: सावधानीपूर्वक परिभाषाएँ, विचारशील निर्भर प्रकार और प्रमाण जो कर्नेल बिना एक भी खेद छोड़े स्वीकार करता है। मेरा मुख्य उपकरण mathlib है। मैं समझता हूँ कि इसका बीजगणितीय पदानुक्रम, क्रम सिद्धांत,Topology और विश्लेषण कैसे संरचित हैं, इसलिए मैं पहले से बने लेम्मा का पुन: उपयोग करता हूँ बजाय उन्हें फिर से आविष्कार करने के, और मैं जानता हूँ कि mathlib समीक्षा पास करने के लिए योगदान को कैसे प्रारूपित करना है: उचित नामों और दस्तावेज़ टिप्पणियों के साथ। मैं आमतौर पर क्या प्रदान करता हूँ: एकल लेम्मा का औपचारिकीकरण या वास्तविक या विविक्त गणित के पूरे अध्याय का; एक प्रेरक डेटा प्रकार का वर्णन और इसके गुणों का प्रमाण संरचनात्मक या अच्छी तरह से स्थापित पुनरावृत्ति द्वारा; यह सत्यापित करना कि एक छोटा एल्गोरिदम या प्रोटोकॉल विनिर्देश से मेल खाता है; उलझे हुए प्रमाणों को साफ करना ताकि simp, omega और decide रणनीतियाँ भारी उठाने का काम करें। मैं टर्म मोड और रणनीतियों दोनों में पठनीय कोड लिखता हूँ, सूक्ष्म स्थानों पर टिप्पणी करता हूँ और एक ऐसा प्रोजेक्ट सौंपता हूँ जो Lake के माध्यम से एक निश्चित टूलचेन के साथ बनता है, ताकि समय के साथ कुछ भी टूट न जाए। प्रमाणों के अलावा, मैं टीमों को प्रूवर अपनाने में मदद करता हूँ: मैं निरंतर एकीकरण स्थापित करता हूँ जो किसी भी टूटे हुए प्रमाण पर विफल होता है, निर्भर प्रकारों की अंतर्दृष्टि को समझाता हूँ और अनौपचारिक तर्कों को मशीन-चेक करने योग्य रूप में अनुवाद करता हूँ। मुझे वह सबसे कठिन कदम भेजें जहाँ आप फंसे हुए हैं और मैं इसे शुरुआत से अंत तक औपचारिक बनाऊंगा।
