Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет borrowedpointer ([info]borrowedpointer)
@ 2026-01-27 18:18:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
формальнологическийвопрос
здравствуйте дорогие матаноёбы. мне одна нейросеть сказала, что в обозримой перспективе llm-ки не освоят пруверы. речь шла про разработку софта, так что всякие f*, lean и прочие dafny. оставим за скобками неготовность индустрии за это платить - врет ли нейросеть? освоят ли блестящие металические зады эту тему, или у людишек есть пара-тройка лет поковыряться там в одиночестве?


(Читать комментарии) - (Добавить комментарий)


(Анонимно)
2026-01-27 13:10 (ссылка)
Если ты посмотришь подробности по ссылке, там видно как это работает уже сейчас
Interestingly, the proof contained some minor errors in it, but the AI tool Aristotle was able to automatically repair these gaps and produce a Lean-verified proof.

и т.д.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]iskramivpeople
2026-01-27 13:18 (ссылка)
Математика и софт ето оч разние задачи какбе

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 13:38 (ссылка)
Я не понимаю, разверните мысль пожалуйста. В посте задан вопрос про софт и математику.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]iskramivpeople
2026-01-27 13:57 (ссылка)
Если для вас не очевидно чем создание и верификация софта
отличаются от создания и доказательства математических
теорем, могу посоветовать классический блог пост из 2016
https://pron.github.io/posts/correctness-and-complexity
там прям по полочкам разложено

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 14:06 (ссылка)
Причем здесь верификация софта?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]iskramivpeople
2026-01-27 14:12 (ссылка)
речь шла про разработку софта

Цитата из оп поста для русских и слабовидящих

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 14:31 (ссылка)
Причем здесь тогда матан, бляди тупые

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]iskramivpeople
2026-01-27 14:36 (ссылка)
Так по ссилке сверху написано при чем матан
Вижу водовка с картофанчиком влияет нехило)

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 15:11 (ссылка)
>проекции

(Ответить) (Уровень выше)


[info]borrowedpointer
2026-01-27 15:40 (ссылка)
сорян что слово матан привело тебя в такое состояние ажитации, но iskramivpeople таки полностью прав

извини за выбор слов

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 16:13 (ссылка)
>проекции

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 20:49 (ссылка)
terpi

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-28 00:57 (ссылка)
пусть скулят и лают сатанисты

(Ответить) (Уровень выше)


[info]phantom
2026-01-27 14:10 (ссылка)
С виду интересно, надо почитать.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 14:11 (ссылка)
Нахуй иди

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 15:11 (ссылка)
Спасибо за комментарий.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2026-01-27 15:12 (ссылка)
Благодарю за понимание

(Ответить) (Уровень выше)


[info]iskramivpeople
2026-01-27 14:13 (ссылка)
Прон -- уберняшка!

(Ответить) (Уровень выше)


(Читать комментарии) -