Post content
Экс-сотрудник Google и сооснователь xAI, объявил о запуске новой компании под названием Mathematics Они создают: Ml-агентов для формализации математики Основной продукт — агент Gauss, построенный на инфраструктуре подкрепленного обучения из Morph Labs Он генерирует тысячи строк кода для доказательств теорем, используя LLM Формальные доказательства сложных теорем Уже на старте они расширили формализацию теоремы о сильном распределении простых чисел Добавили 22.000 строк LLM-генерированного кода в Lean, что делает доказательство полностью проверяемым Инфраструктуру для верифицированного Ml Цель — создать сверхинтеллект, где все выводы не просто генерируются, а строго доказываются Это шаг к Ml, который превзойдёт человека в математике к 2026 году, без "галлюцинаций" или ошибок