Lean 4 માં Collatz Exit-Layer Convergence નું ઔપચારિકીકરણ

હું Lean 4 માં એક નવો પદ્ધતિસરનો (methodological) રેકોર્ડ શેર કરી રહ્યો છું.

આ કાર્ય Collatz dynamics ના એક ચોક્કસ ભાગનું ઔપચારિકીકરણ કરે છે. અમે તેને exit-layer fragment કહીએ છીએ. તે એવા અયુગ્મ સંખ્યાઓને આવરી લે છે જે એક જ સ્ટેપમાં power-of-two સુધી પહોંચે છે.

આ સંપૂર્ણ Collatz conjecture નો પુરાવો નથી. તે જાણીતી ગાણિતિક અવલોકનનો એક ઔપચારિક રેકોર્ડ છે.

મુખ્ય ટેકનિકલ વિગતો:

• અમે orbits ને રજૂ કરવા માટે coinductive Stream' coalgebras નો ઉપયોગ કરીએ છીએ. • અમે Collatz step નો halt-at-1 variant વ્યાખ્યાયિત કરીએ છીએ. • આનાથી orbit અંતે 1 પર સ્થિર (constant) બને છે. • અમે સાબિત કરીએ છીએ કે exit-layer સંખ્યાઓ આ constant stream સુધી પહોંચે છે. • આ પુરાવો પ્રમાણભૂત Mathlib axiom triple પર આધારિત છે.

એક નોંધપાત્ર પરિણામ:

head_collatzOrbit નામનું theorem સંપૂર્ણપણે axiom-free છે. આ theorem પર #print axioms ચલાવવાથી ખાલી સેટ (empty set) મળે છે. આ તેને પ્રમાણભૂત ક્લાસિકલ axiom base થી પણ નીચે લાવે છે.

આ પેપર શું નથી કરતું:

અમારો ધ્યેય અમારા અવલોકિત વ્યાપ (observed range) ની અંદર એક સ્વચ્છ, axiom-free ઔપચારિકીકરણ પૂરું પાડવાનો છે. અમે Kim (2008) ના coalgebraic પરિપ્રેક્ષ્યનો ઉપયોગ કરીએ છીએ અને તેને Lean 4 માં લાગુ કરીએ છીએ.

આ Rei-AIOS શ્રેણીમાં એક પદ્ધતિસરનું યોગદાન છે. તે axiom-base લઘુત્તમીકરણ (minimization) અને જાણીતી સંરચનાઓના ઔપચારિકીકરણ પર ધ્યાન કેન્દ્રિત કરે છે.

સ્ત્રોત: https://dev.to/fc0web/paper-166-v01-a-lean-4-axiom-free-formalization-of-exit-layer-collatz-convergence-as-a-stream-8oi

વૈકલ્પિક લર્નિંગ કોમ્યુનિટી: https://t.me/GyaanSetuAi