Мне нравится комбинировать инструменты ИИ в своих исследованиях, и вот забавная идея, которую, вероятно, никто еще не пробовал. Сначала вы генерируете формальное доказательство с Аристотелем от @HarmonicMath . Затем вы инструктируете @NanoBanana (Pro) с помощью следующего запроса: Создайте иллюстративную инфографику, в которой каждую гипотезу и ее доказательство связывают с конкретным индикатором, который ведет к окончательному выводу (доказательство основной теоремы). Вы руководствуетесь следующим кодом Lean: <Lean code> Счастливого труда!