పాయింకేర్, యంత్రం గీత గీతా తనిఖీ చేసింది

ఒక నిరూపణను తనిఖీ చేయడం గణితంలో అత్యంత శ్రమతో కూడిన పనుల్లో ఒకటి, ముఖ్యంగా ఒక వాదన అనేక రంగాల్లో విస్తరించినప్పుడు. AI నిరూపణల తయారీని వేగవంతం చేస్తున్న కొద్దీ, నమ్మదగిన ధ్రువీకరణ మరింత ముఖ్యమవుతోంది. Lean 4 వంటి నిరూపణ సహాయకాలు (proof assistants) ఒక సమాధానం ఇస్తాయి: నిర్వచనాలు, ప్రవచనాలు, నిరూపణలను కోడ్‌గా రాస్తారు, సాఫ్ట్‌వేర్‌లోని ఒక చిన్న నమ్మదగిన కేంద్రభాగం, దాని “కెర్నల్”, ప్రతి అడుగునూ తనిఖీ చేస్తుంది. కెర్నల్‌ను దాటిన నిరూపణ తన ప్రవచనాన్ని స్థాపిస్తుంది; మనుషులకు మిగిలేది, ఆ ప్రవచనం గణిత శాస్త్రవేత్తలు ఉద్దేశించినదాన్నే నిజంగా చెబుతోందో లేదో చూడటం.

కుదించిన నిరూపణ, లోపించిన లైబ్రరీ

పెరెల్‌మన్ నిరూపించిన పాయింకేర్ ఊహ (Poincaré conjecture), ప్రతి మూసిన, సరళంగా అనుసంధానమైన (simply connected) త్రిమితీయ మానిఫోల్డ్ — అనధికారికంగా చెప్పాలంటే, ఒక ఉచ్చు చిక్కుకునే రంధ్రం లేని పరిమిత 3D ప్రదేశం — త్రిమితీయ గోళానికి సమానమని చెబుతుంది. ఈ నిరూపణ రిచర్డ్ హామిల్టన్ (Richard Hamilton) ప్రారంభించిన రిచీ ఫ్లో (Ricci flow) కార్యక్రమాన్ని అనుసరిస్తుంది. పెరెల్‌మన్ 2002–2003 నాటి మూడు ప్రీప్రింట్లు కీలక వాదనలను అత్యంత కుదించిన రూపంలో ఇచ్చాయి; ఆ తర్వాత వివరణాత్మక వ్యాఖ్యానాలు వచ్చాయి, వాటిలో ఈ ప్రాజెక్టు అనుసరించిన జాన్ మోర్గన్ (John Morgan), గాంగ్ టియాన్ (Gang Tian)ల 2007 నాటి మోనోగ్రాఫ్ ఒకటి.

ఆ నిరూపణ జ్యామితీయ విశ్లేషణపై ఆధారపడుతుంది, Lean కమ్యూనిటీ లైబ్రరీ అయిన Mathlibలో అది చాలావరకు లేదు. పునాదుల్లో చాలా భాగాన్ని మొదటి నుంచి నిర్మించాల్సి వచ్చింది.

గణిత శాస్త్రవేత్తలు స్తంభింపజేసిన మైలురాళ్లు

పెకింగ్ విశ్వవిద్యాలయం, బీజింగ్‌లోని ఇతర సంస్థలకు చెందిన ఝియువాన్ ఝాంగ్ (Zhiyuan Zhang), ఆక్సెల్ దెలవాల్ (Axel Delaval), బిన్ డాంగ్ (Bin Dong), చున్‌లెయ్ లియు (Chunlei Liu), సహచరులు 2026 మేలో మొదలుపెట్టారు: గణిత శిక్షణ ఉన్న ముగ్గురు “AI ఇంజనీర్లు” గణిత శాస్త్రవేత్తలతో కలిసి పనిచేశారు. వారి మొదటి విధానం — నేపథ్య సిద్ధాంతాన్ని పెద్ద పెద్ద భాగాలుగా ఫార్మలైజ్ చేయడం — నెమ్మదిగా సాగింది, దాని నుంచి వచ్చిన కోడ్ వారి అంచనాలను అందుకోలేదు.

2026 సెప్టెంబర్లో వారు మళ్లీ మొదలుపెట్టారు. నిరూపణను సుమారు 90 మైలురాళ్లుగా విభజించారు, ఒక్కొక్కటీ దానికి అవసరమైన నిర్వచనాలతో కూడిన కచ్చితమైన Lean ప్రవచనం. ఈ ప్రవచనాలను ఫార్మలైజ్ చేయడానికి ముందు లేదా చేస్తున్న సమయంలో గణిత శాస్త్రవేత్తలు సమీక్షించారు, ఆ తర్వాత వాటిని స్తంభింపజేశారు: ఏజెంట్లు వాటిని మార్చలేరు, ఏ సవరణైనా గణిత శాస్త్రవేత్తల ద్వారానే జరగాలి. ఏజెంట్లు రాసిన ప్రతి పంక్తినీ ఎవరూ చదవలేరు కాబట్టి, ఈ మైలురాళ్లే మనుషులు గణితాన్ని ధ్రువీకరించే తనిఖీ కేంద్రాలయ్యాయి.

ఆ తర్వాత ఏజెంట్లు సమాంతరంగా పనిచేశారు, కోడింగ్ సాధనాలతో — ప్రధానంగా Codex, Claude Code — పరస్పర చర్చా సెషన్ల ద్వారా, పరిమిత “మిషన్లను” అనేక సర్వర్లకు పంపే Archon Horizon అనే వ్యవస్థ ద్వారా. ఒక బాట్ ప్రతి కృషినీ కంపైల్ చేసి, ఆమోదించినవాటిని విలీనం చేసింది. ప్రవచనాల ఫార్మలైజేషన్, నిరూపణ నిర్మాణంలో ఎక్కువ భాగాన్ని GPT-6-Astra మోసింది; స్వతంత్ర తనిఖీలు, నిలిచిపోయిన పనుల నిర్ధారణ, ప్రవచనాల సమీక్షకు Fable-5.1ను వాడారు.

సుమారు రెండు వారాల్లో 28 లక్షల పంక్తులు

నెలల సన్నాహం తర్వాత, ప్రధాన ఫార్మలైజేషన్‌కు రెండు వారాలకు కొంచెం ఎక్కువ సమయం పట్టింది. AI సబ్‌స్క్రిప్షన్లు, అద్దె సర్వర్ల ఖర్చు సుమారు 25,000 డాలర్లు. ఈ పని సిద్ధాంతపు టోపోలాజికల్, స్మూత్ రెండు రూపాలనూ నిరూపిస్తుంది, పూర్తిగా కంపైల్ అవుతుంది, కేవలం Mathlibతో రాసిన లక్ష్య ప్రవచనాలతో పోల్చే స్వతంత్ర తనిఖీలోనూ నెగ్గుతుంది.

ఇది భారీది: Leanలో సుమారు 32 లక్షల పంక్తులు, తుది సిద్ధాంతం ఆధారపడే భాగాలను మాత్రమే ఉంచితే 28 లక్షలకు తగ్గాయి. రచయితల లెక్క ప్రకారం, దాదాపు సగం నేపథ్య సిద్ధాంతమే. మోర్గన్, టియాన్ ఒకే ఒక్క పాదసూచికలో ప్రస్తావించిన ఒక సంప్రదాయ ఫలితానికి — త్రిమితీయ మానిఫోల్డ్‌లపై స్మూత్ నిర్మాణాల గురించినది — ఒక్కదానికే సుమారు 6,50,000 పంక్తులు పట్టాయి.

మనుషులు ఇంకా చేసినవి

రచయితలు అడ్డంకులను మూడు రకాలుగా విభజిస్తారు: గణిత లోపాలు, Lean అమలు సమస్యలు, సమన్వయ సమస్యలు. మనుషులు ప్రవచనాల పరిధిని నిర్ణయించారు (ఉదాహరణకు, ఒక ఫలితాన్ని త్రిమితీయానికి ఎప్పుడు పరిమితం చేయాలి), లోపించిన వాదనలను గుర్తించారు — ఏజెంట్లు కనుగొనలేని స్థానిక సంక్షిప్తత (local compactness) అడుగు వంటివి — దాగిన ఊహలను పట్టుకున్నారు. వారి ప్రధాన పాఠం: పని వ్యవస్థీకరణ ఏజెంట్ల సామర్థ్యమంత ముఖ్యమైనది. Anthropic ఇటీవల చేసిన ఫెర్మా చివరి సిద్ధాంతపు ఫార్మలైజేషన్ నుంచి కూడా వారు ఇదే నిర్ధారణకు వస్తున్నారు; తొలి ప్రయత్నాలు ప్రాజెక్టు స్థితిని ట్రాక్ చేయలేకపోవడంతో అదీ మళ్లీ మొదలుపెట్టాల్సి వచ్చింది.

ధ్రువీకరించారు, కానీ ఇంకా చక్కదిద్దలేదు

రచయితలు ఈ పని పూర్తయిందని భావించడం లేదు. కోడ్ నిండా పునరావృతాలే; ఏజెంట్ల నిరూపణలు ఎప్పుడూ ప్రామాణిక గ్రంథం మార్గాన్ని అనుసరించవు; దీన్ని మళ్లీ వాడగల జ్యామితీయ విశ్లేషణ లైబ్రరీగా మార్చడమే తదుపరి పని. మరో బృందం అదే ఊహకు స్వతంత్ర ఫార్మలైజేషన్‌ను కూడా ప్రకటించింది. వారి ఆశ: ఏదో ఒక రోజు ఒక్క గణిత శాస్త్రవేత్త అలాంటి సాధనాలతో తన సొంత పరిశోధనను ధ్రువీకరించుకోగలగాలి.

ప్రయోజనాల సంఘర్షణ. బృందం Claude Code, Fable-5.1 మోడల్‌ను వాడింది, రెండూ Anthropicవే; వాటితో పాటు OpenAI సబ్‌స్క్రిప్షన్ల ద్వారా వాడిన GPT-6-Astra ఎక్కువ పని చేసింది. పత్రం తన ప్రాజెక్టును Anthropic చేసిన ఫెర్మా చివరి సిద్ధాంతపు ఫార్మలైజేషన్‌తో కూడా పోలుస్తుంది. ఈ వ్యాసాన్ని Claude రాసింది.