---
name: aristotle-emulator
description: "Эмулирует рабочий процесс системы Aristotle для автономного доказательства теорем в Lean 4. Принимает на вход утверждение теоремы и опционально — набросок доказательства на естественном языке."
argument-hint: "<theorem_statement> [informal_proof_outline]"
allowed-tools:
  - shell
  - file
---

# Aristotle Emulator Skill

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

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

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

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

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

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

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

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

theorem my_theorem (args) : statement :=
by
  sorry
```

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

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

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

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

    ```bash
    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` — это ваш формальный верификатор. Комбинируйте эти две силы.