Automatizácia bez porozumenia: AI dokazuje matematiku, USA škrtí financovanie matematikov

Čo sa stalo

Výskumník Jun-Yong Park zverejnil 12. júla 2026 na arXiv prácu argumentujúcu, že kým AI systémy produkujú legitímnu matematiku — vrátane vyvrátenia Erdosovej planar unit-distance hypotézy — USA súčasne škrtí federálnu podporu pre ľudských matematikov, čím vzniká nebezpečná verifikačná medzera.

Kontext a dopad

Práca prichádza po tom, čo GPT-5.6 Sol dokázal Cycle Double Cover Conjecture za menej ako hodinu. Park tvrdí, že ľudská matematická kapacita na audit AI záverov je nenahraditeľná národná infraštruktúra — jej opätovné vybudovanie trvá dekády. Navrhuje povinný formálny, strojom overiteľný výstup pre dôsledné AI reasoning.

Detaily

• AI vyvrátila Erdosovu planar unit-distance conjecture (2026)
• GPT-5.6 Sol dokázal Cycle Double Cover Conjecture za menej ako hodinu
• USA škrtí federálne financovanie matematikov práve v čase AI rastu
• Navrhovaný liek: povinný formálny (Lean/Coq) výstup pre AI reasoning
• arXiv 2607.06377, 12. júla 2026