Филдсовский лауреат Теренс Тао ведёт на гитхабе страничку, где собраны многие сотни актуальных математических проблем (в основном из базы Эрдёша), которые пытаются решить с помощью AI (в основном жпт и aristotle) или, как минимум, оформить формальные доказательства на каком-нибудь теорем-прувере.

С одной стороны выглядит круто, но с другой стороны если посмотреть, какая там реальная активность -- ну практически никакая. На единичные решения может быть и наберётся 1-2 десятка комментов, а так везде или 0, или кто-нибудь прицепит своё решение и месяцами ждёт, когда оценит/проверит его кто-то (что в целом вообще не факт).

Вообще, похоже, когда что-то делается либо чисто для галочки, либо на голом энтузиазме, когда чел думает: вот сейчас выложу уникальные вещи/идеи в опенсорс, и начнётся движуха. Нет, не начнётся 💯

Пока что на этом в основном только AI-корпорации фейково пиарятся.

Как надо? Нужно прежде всего делать воронку продаж организационный фреймворк, чтобы если делаешь пул-риквест своё условное доказательство, будут гарантии что в разумный срок - например неделю - будет выполнено его ревью, хотя бы предварительное, и потом дадут рекомендацию на публикацию в ведущих математических изданиях.

А как у Тао получается примерно как если бы я сделал "свой теорем-прувер", который работает круче чем Lean, ну и? Можно забросить ссылку в чатик по формальным методам, может 1-2 человека из любопытства заглянут, и быстро забудут.

При том что сам мировой рынок - это ~10 миллиардов долларов.
Intel, AMD, NVIDIA, ARM, автомобильные Tier-1, Airbus, Boeing, медтех используют формальные методы для доказательства корректности архитектур. В финтехе это верификация алгоритмов высокочастотной торговли, протоколы безопасности, уж молчу про крипту и смарт-контракты.
+ Google, Amazon, Microsoft etc вкладывают миллиарды в R&D, где формальные методы применяются к оптимизации компиляторов и ОС, верификации облачной инфраструктуры, создания безошибочных алгоритмов, да и AI тут довольно мощно взлетает.

Наблюдение и думание об math-стартапах продолжаю :)