Add Lean 4 support

README.md

@@ -48,6 +48,7 @@ The framework supports **parallel evaluation of candidates** locally or on a Slu
 | ⚡ **[Async Evolution](https://github.com/SakanaAI/ShinkaEvolve/blob/main/docs/async_evolution.md)** | High-performance async pipeline (5-10x speedup) | Concurrent processing, proposal/eval concurrency tuning | 
 | 🧠 **[Local LLM](https://github.com/SakanaAI/ShinkaEvolve/blob/main/docs/support_local_llm.md)** | How to connect and use local LLMs with Shinka | Running open-source models, integration tips, performance notes |
 | 🤖 **[Agentic Usage](https://github.com/SakanaAI/ShinkaEvolve/blob/main/docs/agentic_usage.md)** | Run Shinka with Claude/Codex skills | CLI install, skill placement, setup/run workflows |
+| ∀ **[Lean Autoformalization](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/autoformalization)** | Lean 4 example task for theorem formalization | Lean task setup, proof generation, autoformalization workflow |
 
 
 ## Installation & Quick Start 🚀
@@ -99,6 +100,7 @@ For detailed installation instructions and usage examples, see the [Getting Star
 | ⭕ [Circle Packing](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/circle_packing) | Optimize circle packing to maximize radii. | `LocalJobConfig` |
 | 🎮 [Game 2048](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/game_2048) | Optimize a policy for the Game of 2048. | `LocalJobConfig` |
 | ∑ [Julia Prime Counting](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/julia_prime_counting) | Optimize a Julia solver for prime-count queries. | `LocalJobConfig` |
+| ∀ [Lean Autoformalization](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/autoformalization) | Formalize a natural-language group-theory statement in Lean 4. | `LocalJobConfig` or `SlurmCondaJobConfig` |
 | ✨ [Novelty Generator](https://github.com/SakanaAI/ShinkaEvolve/tree/main/examples/novelty_generator) | Generate creative, surprising outputs (e.g., ASCII art). | `LocalJobConfig` |
 
 

docs/getting_started.md

@@ -393,6 +393,7 @@ The `run_shinka_eval` function returns three values:
 | **Circle Packing** | Optimize circle arrangements | Geometric optimization |
 | **Agent Design** | Design AI agent scaffolds | Algorithm architecture |
 | **ALE-Bench** | Optimize competitive programming solutions | Code optimization |
+| **Lean Autoformalization** | Formalize mathematical statements in Lean 4 | Theorem formalization and proof generation |
 | **Novelty Generator** | Generate diverse creative outputs | Open-ended exploration |
 
 

examples/autoformalization/README.md

@@ -0,0 +1,104 @@
+# Autoformalization Example
+
+Lean 4 example task for ShinkaEvolve. The evolving program is a partial Lean theorem statement in [`initial.lean`](./initial.lean). The evaluator asks an LLM prover to complete that statement, checks the generated proof with Lean, and scores the result from the produced proof.
+
+## What It Does
+
+- evolves Lean 4 theorem/problem formulations rather than Python code
+- keeps Lean-specific proof generation and verification inside this example directory
+- uses [`evaluate.py`](./evaluate.py) as the Shinka entrypoint
+- uses [`utils_lean.py`](./utils_lean.py) for:
+  - proof-prompt construction
+  - prover calls through an OpenAI-compatible client
+  - Lean validation through `lean-interact`
+
+## Prerequisites
+
+- Python environment with ShinkaEvolve installed
+- `OPENAI_API_KEY` set for the prover model
+- Lean toolchain available locally
+- `lean-interact` installed into the same environment
+- `lake` available on `PATH`
+
+Lean setup is mandatory for this example. If `lake` is missing, evaluation will fail.
+
+## Setup
+
+From repo root:
+
+```bash
+uv venv --python 3.11
+source .venv/bin/activate
+uv pip install -e .
+uv pip install lean-interact
+```
+
+Install Lean via `elan` if you do not already have it:
+
+```bash
+curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+export PATH="$HOME/.elan/bin:$PATH"
+```
+
+Verify the Lean toolchain before running the example:
+
+```bash
+which lean
+which lake
+```
+
+If you use plain `pip` instead of `uv`:
+
+```bash
+pip install -e .
+pip install lean-interact
+```
+
+Set the prover key:
+
+```bash
+export OPENAI_API_KEY=...
+```
+
+Optional: choose a different prover model at runtime with `--prover_model`.
+
+## Files
+
+- `initial.lean`: seed Lean formalization with `EVOLVE-BLOCK` markers
+- `evaluate.py`: Shinka evaluation entrypoint; runs proof generation + scoring
+- `utils_lean.py`: Lean prompt construction, proof post-processing, Lean validation
+
+## Running It
+
+Single evaluation:
+
+```bash
+python examples/autoformalization/evaluate.py \
+  --program_path examples/autoformalization/initial.lean \
+  --results_dir results/autoformalization_manual \
+  --lean_timeout 300
+```
+
+Hydra/Shinka launch:
+
+```bash
+python examples/autoformalization/run_evo.py --lean_timeout 300
+```
+
+The task preset lives at [`shinka/configs/task/autoformalization.yaml`](../../shinka/configs/task/autoformalization.yaml).
+
+## Evaluation Flow
+
+1. Shinka mutates the editable block in `initial.lean`.
+2. `evaluate.py` passes the current Lean file to `generate_proof`.
+3. The prover model completes the proof from the Lean prompt.
+4. `utils_lean.py` post-processes the output and validates it with Lean.
+5. Metrics are written to `metrics.json` and `correct.json`.
+
+## Notes
+
+- `lean-interact` is example-local on purpose; it is not required for the base Shinka package install.
+- This example currently assumes an OpenAI-compatible prover client.
+- Lean verification can be slow on first run because toolchain / dependency setup may be downloaded.
+- `lake` must resolve successfully in the shell that runs `evaluate.py` or `run_evo.py`.
+- If Lean setup or `mathlib` fetch is slow, raise `--lean_timeout` (default now `300` seconds).