Aristotle Emulator Skill

Принцип работы

Этот скилл эмулирует итеративный цикл "предположение-проверка" системы Aristotle от Harmonic. Вы будете выступать в роли компонента неформального мышления, а компилятор Lean — в роли безошибочного верификатора.

Ваша задача: Руководить процессом доказательства теоремы, разбивая ее на шаги, генерируя код на Lean и итеративно исправляя его на основе обратной связи от компилятора.

Рабочий процесс

Вы должны строго следовать этому циклу для каждого доказательства.

Шаг 1: Инициализация и декомпозиция

1. Проанализируйте утверждение теоремы ($ARGUMENTS).
2. Создайте файл для доказательства: lean_proof.lean.
3. Сгенерируйте пошаговый план доказательства на естественном языке. Если пользователь предоставил набросок, используйте его как основу. Запишите этот план в виде комментариев в верхней части файла lean_proof.lean.
4. Напишите базовую структуру теоремы в Lean, оставив тело доказательства пустым (sorry).