Обзор LLM-систем в формальной математике: где современные системы отстают
UCLA
Систематический обзор возможностей LLM в формальной математике (arXiv 2607.07779) в соавторстве с лауреатом медали Филдса Теренсом Тао, охватывающий автоформализацию, синтез доказательств и создание датасетов. Авторы утверждают, что современные системы остаются принципиально ограниченными для открытых исследовательских задач, и описывают разрыв между системами решения доказательств и подлинным математическим исследованием.
Почему это важно
Соавторство лауреата медали Филдса Теренса Тао даёт перспективу наиболее известного математика сообщества на реальное состояние AI-assisted формальной математики.
Важность: 3/5
Систематический обзор возможностей LLM в формальной математике в соавторстве с Теренсом Тао; влиятельное осмысление со стороны ведущего математика мира