Anthropic podle časopisu Nature použil prototyp Claude k převedení důkazu Fermatovy poslední věty do počítačem ověřitelného kódu. Výsledkem je přibližně třináct milionů řádků ve formálním systému Lean. Model dokončil projekt za jedenáct dní, přestože matematici odhadovali, že ruční formalizace by zabrala zhruba deset let. Nejde o nový důkaz původní věty od nuly. Claude pomohl převést existující matematické argumenty do podoby, kterou lze mechanicky kontrolovat. Případ ukazuje rychlý posun v automatizaci formální matematiky, ale také cenu takového výstupu: obrovský objem kódu musí lidé i nástroje dále kontrolovat a udržovat. Nature připomíná, že Anthropic průlom oznámil už 4. září.

Radyz

Radyz publikuje komentáře a praktické texty o AI nástrojích, ChatGPT, Claude a dění kolem OpenAI a Anthropicu. Na webu se soustředí na srozumitelný výklad, vlastní zkušenost a důraz na to, co je pro čtenáře skutečně užitečné.