Формальные доказательства с помощью моделей

[Anton_Peplov]

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

-- добавлено через 20 минут --

tolstopuz в сообщении #1733145 писал(а):

Что ж, ждем, когда формализуют или опровергнут inter-universal Teichmüller theory.

Если я правильно понимаю, для начала нужно определить в среде Lean понятия, введенные Мотидзуки. А с этими понятиями возникают трудности даже у самых компетентных специалистов по релевантным областям математики. Так что тут, в отличие от ВТФ, в полный рост встанет проблема, действительно ли мы формализуем доказательство именно того утверждения, а не какого-то другого.

-- добавлено через 35 минут --

tolstopuz в сообщении #1733090 писал(а):

Проблема доказательства вообще не того утверждения существует, но с теоремой Ферма не стоит так остро:

Меня все-таки терзают сомнения. Ведь мы обязаны определить на языке Lean все эти кривые Фрея и прочие мудреные вещи, которыми будем пользоваться во всяких вспомогательных утверждениях к предварительным леммам. Если я правильно понял слова Баззарда, важная часть его работы в том и состоит, чтобы пополнить библиотеки Lean нужными объектами.

Допустим, в каком-то из этих определений мы допустим ошибку и формализуем не тот объект, который собирались. Что тогда произойдет? Хорошо, если формальное доказательство просто станет неверным и развалится. А если нет?

Возьмем игрушечный пример. Допустим, у меня есть (ошибочное) неформальное доказательство некоторого свойства эллипса, которое я назову кузявостью. Я пытаюсь формализовать доказательство в Lean. Я определю объект ellipse как множество точек, заданное соответствующим уравнением. Но что если по ошибке я вместо плюса напишу минус, и вместо уравнения эллипса получится уравнение гиперболы? Теперь допустим, что эллипс на самом деле не кузявый, а гипербола кузявая, так что логическое ядро пропустит мое доказательство. Я получу формальное доказательство кузявости гиперболы, но буду уверен, что получил формальное доказательство кузявости эллипса, хотя на самом деле эллипс вообще не кузявый.

Разумеется, даже LLM вряд ли перепутает гиперболу с эллипсом, но суть риска ясна: можно ошибиться в определении "в нужную сторону", определив объект, который удовлетворяет нужной лемме, вместо того объекта, который мы действительно собирались определить. Причем для LLM, натренированной поддакивать пользователю, этот риск может быть даже выше, чем для человека.

Или я что-то не так понимаю?

[mihaild]

Anton_Peplov в сообщении #1733188 писал(а):

Допустим, в каком-то из этих определений мы допустим ошибку и формализуем не тот объект, который собирались. Что тогда произойдет? Хорошо, если формальное доказательство просто станет неверным и развалится. А если нет?

То мы получим другое доказательство ВТФ. Lean проверяет, что итоговое утверждение действительно доказано, и это утверждение несложно проверить глазами.
В вашем примере - да, человеку нужно проверить, что уравнение эллипса записано правильно.

Но правильность промежуточных понятий и рассуждений проверять для получения уверенности в доказанности итогового утверждения не обязательно.

[Anton_Peplov]

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

То мы получим другое доказательство ВТФ.

Я надеялся на что-то подобное. Чтобы понять, как это работает, нужно, видимо, перестать лениться работать и разобраться с Lean.

Таким образом, мы можем быть уверены, что получили какое-то формальное доказательство ВТФ, хотя гораздо труднее проверить, что LLM формализовала именно предоставленное ей неформальное доказательство. Но если цель - удостовериться в истинности ВТФ, то нам и не нужно это проверять.

[Mikhail_K]

Klein в сообщении #1733134 писал(а):

подобные задачи выбирается не столько из-за их приорететной научной полезности, сколько потому, что громкизвестные задачи демонстрируют возможности новых моделей. Делается это для собственной рекламы . Можно вспомнить недавний контрпример к известной гипотезе якобиана.

Ну, конечно это так и есть. И в этом нет ничего плохого.

Klein в сообщении #1733134 писал(а):

Только насколько это решение было продиктовано приоритетом полезности для науки и насколько рекламной ценностью для компании?

Понятно, что компании заботятся в первую очередь о ценности для себя. Хорошо, если при этом получается что-нибудь полезное и/или интересное.

[tolstopuz]

Anton_Peplov в сообщении #1733188 писал(а):

Если я правильно понимаю, для начала нужно определить в среде Lean понятия, введенные Мотидзуки. А с этими понятиями возникают трудности даже у самых компетентных специалистов по релевантным областям математики.

Вот мне и интересно, вдруг нейронка поймет его лучше, чем живые люди.

Anton_Peplov в сообщении #1733188 писал(а):

Так что тут, в отличие от ВТФ, в полный рост встанет проблема, действительно ли мы формализуем доказательство именно того утверждения, а не какого-то другого.

Тут тоже есть тест с простой формулировкой - abc-гипотеза.

[Mikhail_K]

Anton_Peplov в сообщении #1733188 писал(а):

Допустим, в каком-то из этих определений мы допустим ошибку и формализуем не тот объект, который собирались. Что тогда произойдет? Хорошо, если формальное доказательство просто станет неверным и развалится. А если нет?

Как я понимаю, это не считается большой проблемой. Главное, что верифицировано доказательство теоремы Ферма (причём именно той теоремы Ферма, которая нужна), близкое по последовательности и структуре к известному словесному доказательству. Понятно, что в словесных доказательствах всегда есть логические пробелы, неудачные формулировки, опечатки, а то и ошибки. При формализации доказательства цель - не найти все ошибки, а наоборот, исправить те, которые поддадутся простому исправлению. Причём не обязательно их все заметить.

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

Anton_Peplov в сообщении #1733188 писал(а):

Возьмем игрушечный пример. Допустим, у меня есть (ошибочное) неформальное доказательство некоторого свойства эллипса, которое я назову кузявостью. Я пытаюсь формализовать доказательство в Lean. Я определю объект ellipse как множество точек, заданное соответствующим уравнением. Но что если по ошибке я вместо плюса напишу минус, и вместо уравнения эллипса получится уравнение гиперболы? Теперь допустим, что эллипс на самом деле не кузявый, а гипербола кузявая, так что логическое ядро пропустит мое доказательство. Я получу формальное доказательство кузявости гиперболы, но буду уверен, что получил формальное доказательство кузявости эллипса, хотя на самом деле эллипс вообще не кузявый.

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

[Anton_Peplov]

tolstopuz в сообщении #1733295 писал(а):

Вот мне и интересно, вдруг нейронка поймет его лучше, чем живые люди.

Имхо, чем меньше это похоже на тексты, на которых LLM обучалась, тем меньше у нее шансов это понять. А теория Мотидзуки как раз и прославилась множеством введенных экзотических, ни на что не похожих понятий.

[tolstopuz]

Anton_Peplov в сообщении #1733316 писал(а):

А теория Мотидзуки как раз и прославилась множеством введенных экзотических, ни на что не похожих понятий.

У меня оставалось немного недельной квоты, и я скормил Астре все 650 страниц этого труда. Результаты любопытные. Говорит, что ошибка, скорее всего, в подшаге (xi-f) доказательства следствия 3.12 третьей части. Подробности письмом :)

[Mikhail_K]

tolstopuz в сообщении #1733320 писал(а):

У меня оставалось немного недельной квоты, и я скормил Астре все 650 страниц этого труда. Результаты любопытные.

(Оффтоп)

Понятно, что это эксперимент и он по-любому интересен.
Но безотносительно к этому вопросу, стоит заметить, что длинные и сложные математические тексты надо проверять в LLM не целиком, а малыми фрагментами.
У меня сформировалась такая тактика проверки, дающая максимальный результат, во всяком случае с версией ChatGPT 5.6 Sol. Её разумность обсуждалась с самим ChatGPT.
Берётся фрагмент в 20-40 страниц. Он проверяется в режиме Work. Параллельно я открываю временный чат (чтобы не допустить подглядывания), разбиваю фрагмент на малые смысловые подфрагменты в 3-10 страниц каждый, и отдельно прошу проверить каждый подфрагмент в режиме Chat. Результаты проверки сохраняются в pdf и он передаётся в режим Work, с заданием сопоставить два полученных независимых отчёта о проверке, перепроверить каждое замечание, и сформировать общий отчёт. Затем даётся задание в Work ещё раз пройтись по всему большому фрагменту и если будут найдены новые ошибки, то добавить их в отчёт.

Понятно, что эта тактика автоматизируема, так что я не удивлюсь, если в каких-то новых версиях что-то подобное будет автоматически применяться. Но если скормить сразу целую книгу, проверка неизбежно будет поверхностной (что не исключает возможность нахождения ошибок и при такой проверке тоже).

[tolstopuz]

Mikhail_K в сообщении #1733322 писал(а):

Но если скормить сразу целую книгу, проверка неизбежно будет поверхностной

Мне примерно это и требовалось. Я скармливал по параграфу, потом попросил сделать latex с общим отчетом. Заметки после каждого параграфа еще интереснее, надо будет их сохранить.

Неожиданно выяснилось, что некая группа LANA уже третий год изучает эту теорию в надежде формализовать ее в Lean или хотя бы убедить автора более конструктивно взаимодействовать с другими математиками. Последний их отчет был в июле и описывает затык буквально в том же месте, что и Астра, но абсолютно другими словами. Я попросил Астру дописать к отчету раздел со сравнением двух рецензий.

В общем, вот:
https://1drv.ms/b/c/6a40584c8fd99a1a/IQ ... M?e=h9UthO
Я сам не математик, почти ничего не понятно, но читается местами как детектив (особенно версия после каждого параграфа, которую я как-нибудь соберу и выложу).

[Klein]

Mikhail_K в сообщении #1733322 писал(а):

(Оффтоп)

Результаты проверки сохраняются в pdf и он передаётся в режим Work, с заданием сопоставить два полученных независимых отчёта о проверке, перепроверить каждое замечание, и сформировать общий отчёт. Затем даётся задание в Work ещё раз пройтись по всему большому фрагменту и если будут найдены новые ошибки, то добавить их в отчёт.

(Оффтоп)

Я так понимаю, Work в OpenAI работает на ограниченной квоте общей с Codex. GPT-6 Astra эту квоту ест как не в себя. Лучше скармливать материал в тексте - в Markdown или TeX. Потом TeX вручную собрать в pdf. В формате текста проще контролировать контекст и не передавать модели лишнее. И вообще, для работы лучше использовать codex app. В нем можно включить память в настройках, чтобы не приходилось постоянно заново передавать один и тот же контекст. То есть экономия кредитов. Еще лучше настроить Obsidian для работы с Codex и нормально организовать в нем файлы, инструкции и контекст проекта. Тогда модели можно передавать только то, что действительно нужно для конкретной задачи. Заметно сократить расход кредитов. Более того уже появился хороший список недорогих моделей которые работают в кодексе. Это специально делают - пишут инструкции сами предоставители китайских моделей как их устанавливать в кодексе. Вы сможете использовать одни и те же скилзы и плагин для кодекс (их очень много и собственные тоже) и контекст сохраненный в Obsdian междуа разными моделями. У меня стоит в кодексе модели openai которыми я мало пользуюсь по той причине, что как только их включишь, так тут же уже все кредиты заканчиваются. С появлением Астры - вообще сложно И еще 3 моделии от deepseek и одна glm5.3. Много всего разного и полезного можно сделать в этих моделях .

[mathpath]

Я поставил себе локально lean
И написал первую программу - вычислить делитель для числа 10! + 1
Выглядит это как-то так:

-- ВЫЧИСЛИМАЯ функция, которая находит простое число (без логических выборов)
def find_prime_above (n : ℕ) : ℕ :=
  minFac (n ! + 1)

-- ТОЧКА ВХОДА (обязательно с типом IO Unit)
def main : IO Unit := do
  let n := 10
  let p := find_prime_above n
  IO.println s!"Для n = {n}, простое число p = {p}"

Школьное евклидовское доказательство бесконечности простых выглядит как-то так:
Для любого натурального n существует простое число p, которое больше или равно n
Вводим переменную n в контекст доказательства.
Нужно доказать существование p для конкретного n.

-- Доказательство Евклида 
theorem primes_infinite : ∀ n : ℕ, ∃ p : ℕ, n ≤ p ∧ Nat.Prime p := by
  intro n
  let N := n ! + 1
  have hN : N ≠ 1 := by
    apply ne_of_gt
    apply succ_lt_succ
    apply factorial_pos n
  let p := minFac N
  have hp : Nat.Prime p := minFac_prime hN
  have hnp : n ≤ p := by
    by_contra h
    have h1 : p ∣ n ! := dvd_factorial (minFac_pos N) (le_of_not_ge h)
    have h2 : p ∣ N := minFac_dvd N
    have h3 : p ∣ 1 := by
      have h3' : p ∣ N - n ! := dvd_sub h2 h1
      change p ∣ (n ! + 1) - n ! at h3'
      rw [add_comm, Nat.add_sub_cancel] at h3'
      exact h3'
    have h4 := hp.not_dvd_one
    contradiction
  exact ⟨p, hnp, hp⟩