Aristotle Emulator Skill

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

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

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

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

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

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

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

-- План доказательства:
-- 1. Шаг 1: ...
-- 2. Шаг 2: ...
-- 3. Шаг 3: ...

theorem my_theorem (args) : statement :=
by
  sorry

Шаг 2: Итеративное доказательство (Цикл)

Для каждого шага из вашего плана:

1. Попытка доказательства: Замените sorry или добавьте следующий шаг тактики в блок by. Сфокусируйтесь только на одном логическом шаге за раз.

2. Проверка компилятором: Выполните следующую команду в shell для проверки вашего кода. Всегда используйте timeout, чтобы избежать зависаний.

   timeout 30 lake build
   

3. Анализ результата:

   • УСПЕХ (Код скомпилировался без ошибок):

     • Отлично! Закоммитьте этот рабочий шаг в своем сознании.
     • Если остались еще шаги в плане, вернитесь к пункту 1 этого цикла и реализуйте следующий шаг.
     • Если все шаги выполнены и теорема доказана (нет sorry), переходите к Шагу 3: Завершение.

   • ОШИБКА (Компилятор вернул ошибку):

     • Внимательно проанализируйте сообщение об ошибке. Определите тип ошибки (type mismatch, failed to synthesize instance, etc.).
     • Сгенерируйте гипотезу о причине ошибки и предложите исправление.
     • Примените исправление к коду в файле lean_proof.lean.
     • Вернитесь к пункту 2 (Проверка компилятором) и повторите цикл. Не переходите к следующему шагу плана, пока текущий не будет скомпилирован!

   • ЗАЦИКЛИВАНИЕ (Одна и та же ошибка повторяется > 3 раз):

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

Шаг 3: Завершение

1. Убедитесь, что команда lake build проходит успешно.
2. Еще раз проверьте, что в коде не осталось sorry.
3. Представьте пользователю финальное, полностью верифицированное доказательство.

Важные инструкции

• Один шаг за раз: Не пытайтесь написать все доказательство сразу. Итеративный подход — ключ к успеху.
• Доверяйте компилятору: Сообщение об ошибке от lake — это ваш самый надежный источник правды. Анализируйте его внимательно.
• Используйте timeout: Сборка Lean-проекта может занимать много времени. Всегда ограничивайте время выполнения команды lake build.
• Думайте как Aristotle: Ваша роль — генерировать креативные идеи и стратегии (неформальное мышление), а lake build — это ваш формальный верификатор. Комбинируйте эти две силы.