Нейросеть+логический движок для математических доказательств

[realeugene]

пианист в сообщении #1706591 писал(а):

Почему не может? Что ей помешает?

Система проверки формальных доказательств.

[mihaild]

пианист в сообщении #1706591 писал(а):

Почему не может? Что ей помешает?

Чекер. В предположении, что в нём нет багов (а проверять формальные доказательства не так уж сложно), он не примет неверное доказательство.

[пианист]

realeugene
mihaild
Ясно, спасибо.

[dsge]

mihaild в сообщении #1706580 писал(а):

что они могут помочь в формализации имеющихся доказательств - перевод с человеческого языка на формальный.

Т.е. делается запрос LLM: "Проверь, пожалуйста, корректность следущей теоремы: ... ". И она переводит формулировку теоремы с человеческого на язык понятный Lean, пересылая далее теорему в Lean в удобном для него формате, тот проверяет и результат отсылает обратно в LLM?

[mihaild]

dsge в сообщении #1706629 писал(а):

Т.е. делается запрос LLM: "Проверь, пожалуйста, корректность следущей теоремы: ... ".

В первую очередь проверка доказательств.
Т.е. человек пишет формулировку в Lean. В LLM идет запрос "вот формулировка, вот неформальное (=как в статьях) доказательство, дай формальное". LLM что-то пишет, отправляет в Lean, тот что-то отвечает, и так 8 раз. Потом LLM выдает что-то, что считает корректным доказательством в Lean, и человек (ну или скрипт, это легко автоматизируется - в общем что-то что умеет делать что попросили) отправляет это финальное доказательство и исходную формулировку в Lean, и если Lean сказал, что всё хорошо - то у нас теперь есть формальное доказательство теоремы (и сопутствующая этому уверенность в её правильности).

[dsge]

mihaild в сообщении #1706632 писал(а):

Т.е. человек пишет формулировку в Lean.

Спасибо! Т.е. LLM является посредником между человеком и Lean.

Попытка испытать ChatGPT; ее ответ, правильный:

Цитата:

Theorem 3.1 is essentially correct: the contraction arguments are present and the inductive scheme is sound. However two small but necessary fixes are required before the proof can be considered fully rigorous in a polished paper

I can produce a short, edited version of the Theorem 3.1 proof (1–2 pages) implementing the two fixes above (the lemma + corrected algebra)

Впечатляет.
Рецензентам тоже облегчается работа.