అక్టోబర్ 6న OpenAI విడుదల చేసిన గణిత సేకరణలో 372 ఫలిత కుటుంబాలుగా క్రమబద్ధీకరించిన 722 మాన్యుస్క్రిప్టులు ఉన్నాయి. ఒక కుటుంబంలో అనేక పత్రాలు ఉండవచ్చు; అధికారిక రుజువు, అనుబంధ మాన్యుస్క్రిప్టులోని వాదనకంటే సంకుచితమైన ప్రకటనను కవర్ చేయవచ్చు. రిపాజిటరీలో పత్రం నుంచి దాని రుజువు అమరిక వరకు అనుసరిస్తే తనిఖీకి ఎంచుకున్న వాదన తెలుస్తుంది.

అక్టోబర్ 7న BIG CHANGE పూర్తి ఫైల్ జాబితా, కేటలాగ్, ఎంచుకున్న రుజువు కళాఖండాలను పరిశీలించింది. ఇది పత్రాలు, స్థిర ఫైళ్ల విశ్లేషణ మాత్రమే; Lean లైబ్రరీని కంపైల్ చేయలేదు, రుజువు తనిఖీదారుని నడపలేదు, గణితాన్ని సమీక్షించలేదు. OpenAI ప్రకటన ఇది దశలవారీ విడుదల అని చెబుతూ, మరిన్ని అధికారికీకరణలు రానున్నాయని పేర్కొంది.

పెద్ద మార్పు

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

మాన్యుస్క్రిప్టులు, కుటుంబాల సంఖ్యలను వేరుగా లెక్కించండి

మా జాబితాలో preprints/ కింద నేరుగా ఉన్న 722 మాన్యుస్క్రిప్ట్ డైరెక్టరీలు కనిపించాయి; ప్రతి దాంట్లో PDF ఉంది. reasoning_traces/ కింద 10 PDFలు ఉన్నాయి. మాన్యుస్క్రిప్ట్ మ్యాప్ లో 372 వేర్వేరు కుటుంబ నమోదులు, 722 మాన్యుస్క్రిప్ట్ లింకులు ఉన్నాయి.

ఈ లెక్కలు వేర్వేరు వస్తువులను సూచిస్తాయి:

కళాఖండం

పాఠకులు పరిశీలించగలది

ఫలిత కుటుంబం

సంబంధిత పత్రాల సమూహం; అనుబంధ వాదనలు, పరిణామాలు లేదా ప్రత్యామ్నాయ రుజువులు ఉండవచ్చు.

మాన్యుస్క్రిప్ట్

సొంత సోర్స్ ఫైళ్లు, citation సమాచారంతో కూడిన గణిత పత్రం.

తార్కిక సారాంశం

ఎంచుకున్న ఫలితంపై మోడల్ తర్కానికి సంక్షిప్త వివరణ.

Lean కళాఖండం

అధికారిక నిర్వచనాలు, ప్రకటనలు, ప్రతిపాదిత రుజువులు; తనిఖీ చేయాల్సినది తెలిపే లింకులు, అమరికలు.

రిపాజిటరీ README ఈ వర్గాలను వివరిస్తూ ధృవీకరణ స్థాయి మారుతుందని హెచ్చరిస్తుంది. కొన్ని ఫలితాలకు Lean అధికారికీకరణ లేదు; అధికారికం కాని పనిలో సమస్యలు ఉండవచ్చని OpenAI చెబుతుంది. అధికారికీకరణ కేటలాగ్ పరిధిని “పాక్షిక పురోగతి”గా, సమీక్ష స్థితిని uncheckedగా నమోదు చేస్తుంది. అవి ప్రచురణ మెటాడేటా మాత్రమే; BIG CHANGE తనిఖీ ఫలితం కాదు.

పబ్లిక్ ఫైళ్లను OpenAI ఖాతా లేకుండా చదవవచ్చు. రూపొందించిన మోడల్ అంతర్గతమని, దాన్ని విడుదల చేయడానికి OpenAI కృషి చేస్తోందని ప్రకటన చెబుతుంది. పత్రాలకు ప్రాప్యత ఉందంటే మోడల్‌కూ ఉందని కాదు.

రుజువును అనుసరించే ముందు వెర్షన్‌ను స్థిరపరచండి

ఇక్కడ వాడిన రిపాజిటరీ స్నాప్‌షాట్ commit adc7f1241b42e322a6451854ab7e4b4c146bf78a; తేదీ అక్టోబర్ 6, 2026, 21:58:50 UTC. ఆ గుర్తింపు ఉన్న లింకులు పరిశీలించిన స్నాప్‌షాట్‌ను స్థిరపరుస్తాయి; main ఉన్నవి మారే డిఫాల్ట్ బ్రాంచ్‌ను అనుసరిస్తాయి. సవరణలు వచ్చినా పాత విడుదలలను ఉంచుతామని OpenAI README చెబుతుంది.

ముందుగా అవలోకనంచూడండి; అది గణిత అంశాల ప్రకారం కుటుంబాలను సమూహపరుస్తుంది. ఆపై మాన్యుస్క్రిప్ట్ మ్యాప్‌తో పత్రాన్ని కనుగొనండి. డైరెక్టరీ పేరు, రిపాజిటరీ commit, citation నమోదు చేయండి. మాన్యుస్క్రిప్ట్ తేదీ, సేకరణ విడుదల తేదీ వేరుగా ఉండవచ్చు.

కుటుంబం 003లో 7/8 కుడివైపు zero-free ప్రాంతం ఉందని చెప్పే పత్రం, 11/12 కుడివైపు ప్రాంతానికి ప్రత్యామ్నాయ రుజువు, Landau–Siegel zerosపై వేరొక పత్రం ఉన్నాయి. మొదటి పత్రం డైరెక్టరీ దాని తేదీ సెప్టెంబర్ 30గా చూపి BibTeX citation ఇస్తుంది. నిర్దిష్ట పత్రాన్ని నమోదు చేయడం వాదనలను వేరు చేస్తుంది.

దాని Lean పరిధి పేజీ అధికారికీకరణ ఏ ప్రకటనలను కవర్ చేస్తుందో, ఏవి మినహాయించబడ్డాయో, తదుపరి అన్వయాలు వదిలివేయబడ్డాయో వివరిస్తుంది. zeta ఫలితం, Dirichlet మరియు Hecke L-functions, ఏకరీతి నిజ-సున్నా అంతరం కోసం వేర్వేరు తనిఖీ ప్రకటనలకు లింక్ చేస్తుంది. ఒకదాన్ని తనిఖీ చేయడం మిగతావన్నీ తనిఖీ చేసినట్లు కాదు.

ఎంచుకున్న ప్రకటనను దాని అమరిక వరకు అనుసరించండి

OpenAI యొక్క Comparator సూచనలు కుటుంబం 003ను ఉదాహరణగా తీసుకుంటాయి. Comparator ప్రతిపాదిత Lean రుజువును పేర్కొన్న challengeతో పోల్చే సాధనం. ఉదాహరణ JSON అమరిక ఒక సిద్ధాంతాన్ని ఎంచుకుంటుంది: వాదనలోని నిజ భాగం 7/8 కంటే ఎక్కువైతే Riemann zeta ఫంక్షన్ nonzero అవుతుంది.

అమరిక challenge module, వేరొక solution moduleను సూచిస్తుంది. ఇది ప్రామాణిక axioms propext, Quot.sound మరియు Classical.choiceను అనుమతించి, enable_nanoda ను falseగా సెట్ చేస్తుంది. Nanoda అనేది Comparator వాడగల స్వతంత్ర checker; ఈ అమరిక దాన్ని ఎనేబుల్ చేయదు.

ఈ challenge file లో sorry, Leanలో అసంపూర్ణ proofకు placeholder. ఇక్కడ దాని పాత్ర నిర్దిష్టం: సరిపోల్చాల్సిన statementను అందిస్తుంది. Comparator documentation challengeలో placeholderను అనుమతిస్తుంది; solutionలో సరైన proofను కోరుతుంది. Finding sorry ఈ challengeలో మాత్రమే ఉందని కనుగొనడం వేరే solution ఉత్తీర్ణమవుతుందో చెప్పదు. Comparator documentation.

పత్రబద్ధం చేసిన స్థానిక తనిఖీకి ఈ configuration, దాని challenge మరియు solution modules, వాటి dependencies ఇన్‌పుట్‌గా అవసరం. రిపాజిటరీ pin చేసిన వెర్షన్ Lean 4.34.1. దాని Lake manifest Mathlib సహా dependency revisionsను నమోదు చేస్తుంది; Mathlib revision d13f23b723b8a846827a245b89c10fc7d3f11612 .

OpenAI comparator మరియు landrun తో పాటు lean4export ను executable search pathలో ఉంచాలని కోరుతుంది; తర్వాత ఈ commandsను lean/ directory నుంచి నడపాలని వివరిస్తుంది:

Terminal
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

ఇవి ప్రచురణకర్త సూచనలు మాత్రమే; మేము నడిపిన commands కావు. ఆ మూడు బాహ్య toolsకు వెర్షన్లు pin చేయలేదు. Comparator ప్రస్తుత documentation అనుకూలమైన lean4exportను కోరుతుంది; sandbox ముందస్తు అవసరాలు, challengeతో సరిపోలిక, అనుమతించిన axioms వినియోగం, kernel అంగీకారం విజయంగా పరిగణించే షరతులను వివరిస్తుంది. తిరిగి అమలు చేయగల నివేదికలో repository commitతో పాటు install చేసిన tool versions, వాస్తవ output ఉండాలి.

ఈ Lean library README పెద్ద libraryలోని చిన్న భాగాలను compile చేయాలని సిఫార్సు చేస్తుంది. Linux memory-mapping పరిమితుల వల్ల పూర్తి build ఆగిపోవచ్చని కూడా చెబుతుంది. ఈ ఉదాహరణకు స్థానిక runtime లేదా hardware ఖర్చును మేము కొలవలేదు.

విజయవంతమైన తనిఖీని ప్రకటిత పరిధిలో చదవండి

Lean యొక్క validation reference, చూసినప్పుడు వెర్షన్ 4.35.0-rc3, formal proofను అంగీకరించడం, theorem అర్థాన్ని వ్యాఖ్యానించడం వేర్వేరని చెబుతుంది. ఈ documentation వెర్షన్ రిపాజిటరీలో pin చేసిన toolchainకు వేరు.

ప్రాథమిక తనిఖీ విజయవంతమైతే, నిర్వచనాలు, imports, axioms కింద kernel formal statementను అంగీకరించిందని అర్థం. dependenciesలో అసంపూర్ణ proofs ఉండవచ్చు. ఉపయోగించిన axiomsను చూపేందుకు Lean #print axioms ను వివరిస్తుంది; dependency chainలో అసంపూర్ణ proofకు sorryAx ఉంటుంది.

మరింత బలమైన తనిఖీలు నిల్వ చేసిన proofsను మళ్లీ నడపవచ్చు లేదా solutionను విడిగా నిర్దేశించిన statementతో పోల్చవచ్చు. అవి checking environmentపై, ఉద్దేశించిన అర్థం సరిగ్గా వ్యక్తమైందా అన్నదానిపై ఆధారపడతాయి. అందుకే ఖచ్చితమైన challenge, అనుమతించిన axioms, external checker settingsను verification reportలో నమోదు చేయాలి. Kernel acceptance గానీ challengeతో match గానీ journal acceptanceను లేదా manuscriptలోని ప్రతి claim formalize అయిందని నిరూపించవు.

compute సంఖ్య generationను వివరిస్తుంది

సగటున ఒక్కో ఫలితానికి ChatGPT Proలో సుమారు మూడు గంటలు ఆలోచించినంత computing effort వాడినట్లు OpenAI చెబుతుంది. README ప్రకారం evaluationలో సుమారు 4,000 సమస్యలు ఇచ్చి, outputsను సమూహపరచి ముఖ్యమైన వాటిని ఎంచుకున్నారు. సాధారణ ప్రక్రియలోని మినహాయింపులనూ ఇది పేర్కొంటుంది. ఇవి సంస్థ generation గణాంకాలు; పాఠకుడి Lean తనిఖీ ధరను లేదా మొత్తం డాలర్ బిల్లును ఇవ్వవు. విడుదల ప్రకటన, generation వివరణ.

Family 003పై ఈ పరిశీలన నిర్దిష్ట zeta statement, ప్రతిపాదిత solution, checker అనుమతించే axiomsను గుర్తిస్తుంది. అందించిన ఉదాహరణలో Nanoda ఆఫ్‌లో ఉందని కూడా నిర్ధారిస్తుంది. ఈ configurationతో తనిఖీ విజయవంతమవుతుందో లేదో, దాన్ని నడిపి నమోదు చేసినప్పుడే తెలుస్తుంది.

మూలాలు, మరింత చదవడానికి

  • అక్టోబర్ 6 OpenAI ప్రకటనవిడుదల తేదీ, మోడల్ అంతర్గత స్థితి, ప్రణాళికలోని చేర్పులు, కంపెనీ compute అంచనాను నిర్ధారిస్తుంది. ఇది developer తన పని గురించి చెప్పిన వివరణ.
  • pin చేసిన రిపాజిటరీఇక్కడ పరిశీలించిన catalogue, manuscript files, proof configurationsను అందిస్తుంది. సంఖ్యలు పూర్తి inventory, manuscript map నుంచి వచ్చాయి; ఎంచుకున్న formal filesను నడపకుండా చదివాం. నిర్మాణం తెలుసుకోవడానికి overview LaTeX sourceను పరిశీలించాం.
  • Lean validation referenceproof checking అర్థం, పరిమితులను వివరిస్తుంది. మేము 4.35.0-rc3 referenceను వాడాం; OpenAI project Lean 4.34.1ను pin చేస్తుంది.
  • Comparator documentationchallenge, solution files, environment అవసరాలు, షరతులతో కూడిన హామీలను వివరిస్తుంది. ఈ collectionకు verification ఫలితాన్ని నివేదించదు.
  • Curtis Pyke Kingy.ai సమీక్షవిడుదలపై స్వతంత్ర static పరిశీలనను అందిస్తుంది. స్వతంత్ర Lean execution జరగలేదని స్పష్టంగా చెబుతుంది; proof check పునరుత్పత్తిగా మేము దీన్ని పరిగణించం.
  • BIG CHANGE మునుపటి AI గణిత కథనంమే నుంచి సెప్టెంబర్ వరకు పరిణామాలను కవర్ చేస్తుంది. ఈ కథనం కొత్త collection artifact నిర్మాణం, పరిశీలనా విధానాన్ని చూస్తుంది.