Нактнулся тут на адрес
https://lean-lang.org/eval/Там дан список (нетривиальных) теорем и для каждой из них фиксируются попытки формально доказать их в Lean с помощью нейронок. Теорему Ферма, понятное дело, не доказал (не успел доказать) никто, но потрясла одна вещь.
https://lean-lang.org/eval/problems/feit_thompson/Теорема Фейта-Томпсона о разрешимости групп нечетного порядка. В 2012 году ее формальное доказательство в Coq (ныне Rocq) было подвигом. Сейчас ее в Lean с помощью нейронок доказали уже четверо. Я, правда, до конца не понял, кто доказывал на основе текста, а кто просто отпортил доказательство Coq, но у кого-то из четверых я, кажется, встречал упоминание "потребовалась еще пара книжек, формализуем и их тоже".
