GitHub-радар
OpenAI Ten Proofs: математические доказательства в Lean 4
OpenAI опубликовал машинно-проверяемые доказательства на Lean 4 для десяти результатов в математике и теоретической информатике — от упаковки шаров и теории Рамси до квантовых игр и сложности схем.
Десять новых теорем в математике и теоретической информатике, доказанных с полностью проверенными машиной доказательствами на Lean 4. Двоичные коды, сферические коды, несофические группы, гипотеза жёсткости Конна, повторение квантовых игр, задача о ближайшем векторе, гипотеза Erhart об объёме, многоцветные числа Рамсея, экстремальная комбинаторика.
Зачем это вайб-кодеру
ИИ начинает помогать решать задачи в тех областях математики, которые не поддавались решению десятилетиями. Мы также получаем количественную оценку успехов ИИ в логическом мышлении, видя, что доказательства полностью прозрачны для машин.
▌ Ещё находки