వార్తల్లో ఎందుకు?
ఆంత్రోపిక్ (Anthropic) తన క్లాడ్ (Claude) సిస్టమ్ ఫెర్మాట్ (Fermat) చివరి సిద్ధాంతం యొక్క పూర్తి కంప్యూటర్-చెక్డ్ రుజువును తయారు చేసిందని 4 సెప్టెంబర్ 2026న ప్రకటించింది. ఈ ఎడిషన్లో సిద్ధాంతం యొక్క పునరుద్ధరించబడిన కవరేజ్ వెనుక ఉన్న అభివృద్ధి ఈ ప్రకటన. ఆండ్రూ విల్స్ (Andrew Wiles) ఇప్పటికే ఫలితాన్ని స్థిరపరిచారు, ప్రచురించిన రుజువు 1995లో కనిపించింది. కొత్తది ఏమిటంటే లాంఛనప్రాయం (formalisation): ప్రూఫ్-చెక్కింగ్ ప్రోగ్రామ్ దశల వారీగా పరిశీలించగల భాషలో తార్కికతను వ్యక్తపరచడం. ఈ పని లీన్ (Lean) ను ఉపయోగించిందని మరియు ఎక్కువగా అటానమస్ యాక్టివిటీతో పదకొండు రోజులు పట్టిందని ఆంత్రోపిక్ చెబుతోంది. ఇది పబ్లిక్ రీసెర్చ్ రిపోజిటరీ ద్వారా మద్దతు పొందిన కంపెనీ-రిపోర్ట్ చేసిన విజయం, సిద్ధాంతం యొక్క కొత్త ఆవిష్కరణ కాదు. సుదీర్ఘ గణిత వాదనలను చేతితో సమగ్రంగా తనిఖీ చేయడం కష్టం కాబట్టి ఇది ముఖ్యమైనది. అధికారిక ప్రకటన మరియు దాని అంచనాలు ఉద్దేశించిన గణితానికి సరిపోలితే, మెషిన్ చెకింగ్ కఠినమైన ధ్రువీకరణ మార్గాన్ని జోడించగలదు.
కష్టమైన సిద్ధాంతం వెనుక ఉన్న సాధారణ ప్రశ్న
సిద్ధాంతం an + bn = cn సమీకరణానికి సంబంధించినది. ఘాతాంకం రెండు ఉన్నప్పుడు, ధనాత్మక పూర్ణ-సంఖ్య పరిష్కారాలు ఉన్నాయి: 3² + 4² = 5², ఎందుకంటే 9 + 16 = 25. ఘాతాంకం రెండు కంటే ఎక్కువ పూర్ణాంకం ఉన్నప్పుడు అటువంటి పరిష్కారం ఏదీ ఉండదని ఫెర్మాట్ దావా.
సానుకూల పూర్ణాంకాల పరిమితి అవసరం. ఇది పేర్కొన్న సమస్య నుండి సున్నా, ప్రతికూల విలువలు మరియు భిన్నాలను మినహాయిస్తుంది. సున్నాను అనుమతించడం వెంటనే 0n + 1n = 1n వంటి ఉదాహరణలను సృష్టిస్తుంది. అది ఫెర్మాట్ సిద్ధాంతానికి విరుద్ధంగా ఉండదు; ఇది అడుగుతున్న ప్రశ్న పరిస్థితులను మారుస్తుంది.
సాధ్యమయ్యే అనేక సంఖ్యలను పరీక్షించడం ప్రతి సానుకూల పూర్ణాంకానికి వాదనను నిరూపించదు. పరిగణించడానికి అనంతమైన కలయికలు మరియు ఘాతాంకాలు ఉన్నాయి. భారీ శోధనలో ఎటువంటి మినహాయింపు కనుగొనబడలేదని నివేదించడం కంటే రుజువు వాటన్నింటినీ కవర్ చేసే కారణాన్ని తప్పనిసరిగా ఏర్పాటు చేయాలి. ఈ వ్యత్యాసం గణిత రుజువును ఆకట్టుకునే సంఖ్యా ప్రయోగం నుండి వేరు చేస్తుంది.
విల్స్ పని ఇప్పటికే సాధించినది ఏమిటి
ఫెర్మాట్ పదిహేడవ శతాబ్దంలో సమస్యను పేర్కొన్నాడు, అయితే ఒక సాధారణ రుజువు శతాబ్దాలుగా అంతుచిక్కలేదు. విల్స్ 1994లో రిచర్డ్ టేలర్ (Richard Taylor) నుండి ముఖ్యమైన సహకారంతో నిర్ణయాత్మక పనిని పూర్తి చేశాడు. పత్రాలు 1995లో కనిపించాయి. పూర్తి మరియు ప్రచురణ తేదీలను వేరుగా ఉంచడం వల్ల ఒకే పురోగతి యొక్క రెండు వివరణలు విరుద్ధంగా అనిపించవు.
రుజువు చేసే మార్గం ఫెర్మాట్ సమీకరణాన్ని ఎలిప్టిక్ కర్వ్లు మరియు మాడ్యులర్ ఫారమ్లతో కలుపుతుంది. ఎలిప్టిక్ కర్వ్లు అనేవి నిర్దిష్ట క్యూబిక్ సమీకరణాల ద్వారా వర్ణించబడిన గణిత వస్తువులు, సాధారణ ఎలిప్స్లు కాదు. మాడ్యులర్ ఫారమ్లు అత్యంత నిర్మాణాత్మక విధులు. మునుపటి పని ఫెర్మాట్ వాదనకు అసాధారణమైన మినహాయింపును సరిపోలని గణిత లక్షణాలను కలిగి ఉన్న దీర్ఘవృత్తాకార వక్రతతో ముడిపెట్టింది.
విల్స్ సెమీస్టేబుల్ ఎలిప్టిక్ కర్వ్స్ అనే తరగతికి అవసరమైన మాడ్యులారిటీ ఫలితాన్ని ఏర్పాటు చేశాడు. మునుపటి కనెక్షన్తో కలిపి, ఇది ఊహాజనిత మినహాయింపును తోసిపుచ్చింది. అబెల్ ప్రైజ్ (Abel Prize) యొక్క అనులేఖనం ఆ ఆలోచనల గొలుసును వివరిస్తుంది. అందువల్ల ఈ విజయం సంఖ్యల ద్వారా అంతులేని శోధన కాదు కానీ గణితంలోని వివిధ రంగాలను అనుసంధానించే నిర్మాణ వాదన.
లీన్ దేనిని తనిఖీ చేస్తుంది
శిక్షణ పొందిన రీడర్ వాటిని సరఫరా చేయగలడు కాబట్టి వ్రాతపూర్వక రుజువు తరచుగా సాధారణ దశలను చెప్పకుండా వదిలివేస్తుంది. లాంఛనప్రాయం నిర్వచనాలు మరియు తార్కిక ఆధారపడటాలను సాఫ్ట్వేర్ కోసం తగినంత ఖచ్చితమైనదిగా చేస్తుంది. లీన్ అనేది ఈ ప్రయోజనం కోసం ఉపయోగించే ప్రోగ్రామింగ్ లాంగ్వేజ్ మరియు ప్రూఫ్ అసిస్టెంట్. ప్రూఫ్ అసిస్టెంట్ అనేది అధికారిక గణిత వాదనలను నిర్మించడానికి మరియు తనిఖీ చేయడానికి ఒక వ్యవస్థ.
లీన్ యొక్క డాక్యుమెంటేషన్ రుజువును నిర్మించడంలో సహాయపడే సాధనాలను దానిని తనిఖీ చేసే చిన్న విశ్వసనీయ భాగం నుండి వేరు చేస్తుంది. ఆ భాగాన్ని కర్నెల్ అంటారు. ఆటోమేటెడ్ పద్ధతులు రీజనింగ్ను ప్రతిపాదించగలవు లేదా సమీకరించగలవు, అయితే ఫలితంగా వచ్చే ప్రూఫ్ ఆబ్జెక్ట్ చెకింగ్ నిబంధనలను తప్పక సంతృప్తిపరచాలి. నిష్కళంకమైన వివరణాత్మక వచనం దానంతటదే అంగీకరించబడిన రుజువు కాదు.
ఇది ఉత్పత్తి మరియు ధ్రువీకరణ మధ్య ఉపయోగకరమైన విభజనను సృష్టిస్తుంది. వాదన కోసం వెతుకుతున్నప్పుడు సిస్టమ్ విఫల ప్రయత్నాలు చేయవచ్చు; ఆ ప్రయత్నాలు కాన్ఫిడెంట్గా ఉత్పత్తి అయినందున మాత్రమే ధ్రువీకరించబడవు. ముఖ్యమైనది తుది అధికారిక ప్రకటన, అది ఉపయోగించే అంచనాలు మరియు ఆ అంచనాలను ముగింపుకు అనుసంధానించే తనిఖీ చేయబడిన తార్కికం.
పబ్లిక్ విడుదల క్లెయిమ్ చేస్తున్నది ఏమిటి
ఆంత్రోపిక్ మొదటి పూర్తి కంప్యూటర్-చెక్డ్ రుజువుగా విడుదలను వివరిస్తుంది మరియు సుమారు పదమూడు మిలియన్ లైన్ల లీన్ కోడ్ను నివేదిస్తుంది. ఆ స్థాయి మరియు ప్రాధాన్యత క్లెయిమ్లు కంపెనీ ఖాతాకు చెందుతాయి. నిర్వచనాలు, లైబ్రరీలు లేదా మునుపటి లాంఛనప్రాయ ప్రయత్నాలు లేకుండా ప్రారంభించకుండా, మానవ గణితం మరియు ఇప్పటికే ఉన్న ఓపెన్ సోర్స్ ప్రాజెక్ట్లపై ఈ పని నిర్మించబడుతుంది.
రిపోజిటరీ సానుకూల సహజ సంఖ్యలు మరియు కనీసం మూడు ఘాతాంకాలను ఉపయోగించి ఫెర్మాట్ ఫలితాన్ని తెలియజేస్తుంది. ఇది అసంపూర్తి ప్రూఫ్ ప్లేస్హోల్డర్లను మినహాయించడానికి ఉద్దేశించిన తనిఖీలను మరియు లీన్ యొక్క ప్రామాణిక పునాదులకు మించి అదనపు అంచనాలను వివరిస్తుంది. ఇది రెండవ కర్నెల్ అమలును ఉపయోగించి ధ్రువీకరణను కూడా నివేదిస్తుంది. పాఠకులను ప్రచార శీర్షికపై మాత్రమే ఆధారపడేలా కోరడం కంటే ఈ రికార్డులు తనిఖీ విధానాన్ని తనిఖీ చేసేలా చేస్తాయి.
అధికారిక ప్రతిపాదనను తనిఖీ చేయడానికి మరియు అది ఉద్దేశించిన వాస్తవ ప్రశ్నను వ్యక్తపరుస్తుందా అని నిర్ణయించడానికి మధ్య ఇంకా వ్యత్యాసం ఉంది. మార్చబడిన నిర్వచనాలతో కరెక్ట్గా ధ్రువీకరించబడిన స్టేట్మెంట్ వేరేదాన్ని నిరూపించగలదు. రిపోజిటరీ మ్యాచింగ్ స్టేట్మెంట్ను స్పష్టంగా పరిష్కరిస్తుంది. లీన్ యొక్క సొంత మార్గదర్శకత్వం విశ్వసనీయ పునాదులను మరియు ఖచ్చితమైన సూత్రీకరణను రుజువును అంచనా వేయడంలో భాగంగా పరిగణిస్తుంది.
ముగింపు
సెప్టెంబరు డెవలప్మెంట్ స్థిరమైన గణిత శాస్త్రం కోసం కొత్త వెరిఫికేషన్ ఆర్టిఫ్యాక్ట్కు సంబంధించినది, ఫెర్మాట్ సమస్య యొక్క మొదటి పరిష్కారం కాదు. యాంత్రిక తనిఖీ మరియు తదుపరి తనిఖీకి తార్కిక గొలుసును అందుబాటులో ఉంచడంలో దీని ప్రాముఖ్యత ఉంది. శాశ్వత సహకారం కేవలం రూపొందించిన కోడ్ యొక్క వేగం లేదా వాల్యూమ్పై కాకుండా ఆ అధికారిక పని యొక్క విశ్వసనీయత మరియు పునర్వినియోగంపై ఆధారపడి ఉంటుంది.