Поэтому история AlphaProof Nexus интересна именно формальной проверкой, а не просто тем, что «модель что-то решила». Девять задач из 353 звучит скромно, но для открытых проблем это уже не игрушечный результат. Внутри разобрал, почему связка LLM + Lean может быть важнее очередного большого бенчмарка. AlphaProof Nexus решил 9 открытых задач Эрдёша
Математика обычно плохо поддаётся AI-хайпу: красивый ответ ничего не значит, если доказательство разваливается на первом строгом шаге. Поэтому история AlphaProof Nexus интересна именно формальной проверкой, а не просто тем, что «модель что-то решила». Девять задач из 353 звучит скромно, но для открытых проблем это уже не игрушечный результат. Внутри разобрал, почему связка LLM + Lean может быть важнее очередного большого бенчмарка.
AlphaProof Nexus решил 9 открытых задач Эрдёша
