Add Lean 4 support

README.md

@@ -7,16 +7,16 @@
   <img src="https://img.shields.io/badge/python-%3E%3D3.10-blue" />
   <a href="https://github.com/SakanaAI/ShinkaEvolve/blob/master/LICENSE.md"><img src="https://img.shields.io/badge/license-Apache2.0-blue.svg" /></a>
   <a href="https://github.com/astral-sh/ruff"><img src="https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/astral-sh/ruff/main/assets/badge/v2.json" /></a>
-  <a href="http://arxiv.org/abs/2212.04180"><img src="http://img.shields.io/badge/paper-arxiv.2212.04180-B31B1B.svg" /></a>
+  <a href="http://arxiv.org/abs/2509.19349"><img src="http://img.shields.io/badge/paper-arxiv.2509.19349-B31B1B.svg" /></a>
   <a href="https://colab.research.google.com/github/SakanaAI/ShinkaEvolve/blob/main/examples/shinka_tutorial.ipynb"><img src="https://colab.research.google.com/assets/colab-badge.svg" /></a>
 </p>
 
 
-`ShinkaEvolve` is a framework that combines Large Language Models (LLMs) with evolutionary algorithms to drive scientific discovery. By leveraging the creative capabilities of LLMs and the optimization power of evolutionary search, `ShinkaEvolve` enables automated exploration and improvement of scientific code. The system is inspired by the [AI Scientist](https://sakana.ai/ai-scientist/), [AlphaEvolve](https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/) and the [Darwin Goedel Machine](https://sakana.ai/dgm/): It maintains a population of programs that evolve over generations, with an ensemble of LLMs acting as intelligent mutation operators that suggest code improvements.
+[`ShinkaEvolve`](https://arxiv.org/abs/2509.19349) is a framework that combines Large Language Models (LLMs) with evolutionary algorithms to drive scientific discovery. By leveraging the creative capabilities of LLMs and the optimization power of evolutionary search, `ShinkaEvolve` enables automated exploration and improvement of scientific code. The system is inspired by the [AI Scientist](https://sakana.ai/ai-scientist/), [AlphaEvolve](https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/) and the [Darwin Goedel Machine](https://sakana.ai/dgm/): It maintains a population of programs that evolve over generations, with an ensemble of LLMs acting as intelligent mutation operators that suggest code improvements.
 
 The framework supports **parallel evaluation of candidates** locally or on a Slurm cluster. It maintains an archive of successful solutions, enabling knowledge transfer between different evolutionary islands. `ShinkaEvolve` is particularly well-suited for scientific tasks where there is a verifier available and the goal is to optimize performance metrics while maintaining code correctness and readability.
 
-![](docs/conceptual.png)
+![evolution](https://github.com/user-attachments/assets/22cf3468-17fe-4995-9e13-d602b490a54e)
 
 ## Documentation 📝
 
@@ -26,6 +26,7 @@ The framework supports **parallel evaluation of candidates** locally or on a Slu
 | 📓 **[Tutorial Notebook](examples/shinka_tutorial.ipynb)** | Interactive walkthrough of Shinka features | Hands-on examples, configuration, best practices |
 | ⚙️ **[Configuration](docs/configuration.md)** | Comprehensive configuration reference | All config options, optimization settings, advanced features |
 | 🎨 **[WebUI](docs/webui.md)** | Interactive visualization and monitoring | Real-time tracking, result analysis, debugging tools | 
+|🕹️ **[Local LLM Support](https://github.com/SakanaAI/ShinkaEvolve/blob/main/docs/support_local_llm.md)**| Instructions for Local LLMs | How to setup local LLMs on your machine|
 
 ## Installation & Quick Start 🚀
 
@@ -52,9 +53,9 @@ For detailed installation instructions and usage examples, see the [Getting Star
 | Example | Description | Environment Setup |
 |---------|-------------|-------------------|
 | ⭕ [Circle Packing](examples/circle_packing) | Optimize circle packing to maximize radii. | `LocalJobConfig` |
-| 🤖 [Agent Design](examples/agent_design) | Design agent scaffolds for math tasks. | `LocalJobConfig` |
+| 🤖 [Agent Design](examples/adas_aime) | Design agent scaffolds for math tasks. | `LocalJobConfig` |
 | 🎯 [ALE-Bench](examples/ale_bench) | Code optimization for ALE-Bench tasks. | `LocalJobConfig` |
-| ✨ [Novelty Generator](examples/novelty_generator_bck) | Generate creative, surprising outputs (e.g., ASCII art). | `LocalJobConfig` |
+| ✨ [Novelty Generator](examples/novelty_generator) | Generate creative, surprising outputs (e.g., ASCII art). | `LocalJobConfig` |
 
 
 ## `shinka` Run with Python API 🐍
@@ -308,9 +309,9 @@ If you use `ShinkaEvolve` in your research, please cite it as follows:
 
 ```
 @article{lange2025shinka,
-  title={ShinkaEvolve: Towards Open-Ended and Sample-Efficient Program Evolution},
+  title={ShinkaEvolve: Towards Open-Ended And Sample-Efficient Program Evolution},
   author={Lange, Robert Tjarko and Imajuku, Yuki and Cetin, Edoardo},
-  journal={arXiv preprint},
+  journal={arXiv preprint arXiv:2509.19349},
   year={2025}
 }
-```
+```

configs/config.yaml

@@ -2,9 +2,9 @@ defaults:
   - _self_
   - database@_global_: island_small
   - evolution@_global_: small_budget
-  - task@_global_: mad_tf
+  - task@_global_: circle_packing
   - cluster@_global_: local
-  - variant@_global_: mad_tf_example
+  - variant@_global_: circle_packing_example
 
 verbose: false
 results_dir: results

configs/task/autoformalization.yaml

@@ -0,0 +1,49 @@
+evaluate_function:
+  _target_: examples.autoformalization.evaluate.main
+  program_path: ???
+  results_dir: ???
+
+distributed_job_config:
+  _target_: shinka.launch.SlurmCondaJobConfig
+  modules:
+  - "cuda/12.4"
+  - "cudnn/8.9.7"
+  - "hpcx/2.20"
+  eval_program_path: "shinka/eval_hydra.py"
+  conda_env: "shinka"
+  time: "01:00:00"
+  cpus: 16
+  gpus: 1
+  mem: "8G"
+
+evo_config:
+  task_sys_msg: |
+    You are an expert mathematician with a specialization in group theory. You want to prove the following statement:
+
+    "Let $H$ be the subgroup generated by two elements $a, b$ of a group $G$. Prove that if $a b=b a$, then $H$ is an abelian group."
+
+    Your task is to identify the minimal set of variables and assumptions needed to formalize the proof in Lean 4. You do not have to provide the proof itself. Therefore, your output is expected to look like:
+
+    ```lean
+    -- Variables
+    theorem abelian_group (<Write the variables needed for the proof here>)
+    -- Assumptions
+    <Write the assumptions needed for the proof here>
+    :
+    -- Conjecture
+    (<Write the proof's conjecture here>)
+    :=
+    ```
+
+    Key components to add:
+    1. Introduce all variables you need to complete the proof.
+    2. Write all assumptions needed to complete the proof.
+    3. Think about a conjecture that reflects the scientific concept you want to prove. 
+
+    Make sure your output is valid Lean 4. Do not leave the conjecture empty `()`. Do **not** finish the proof, you can leave the program up to the `:=` sign. 
+
+  language: "lean"
+  init_program_path: "examples/autoformalization/initial.lean"
+  job_type: "slurm_conda"
+
+exp_name: "shinka_autoformalization"

configs/variant/autoformalization_example.yaml

@@ -0,0 +1,8 @@
+defaults:
+  - override /database@_global_: island_small
+  - override /evolution@_global_: small_budget
+  - override /task@_global_: autoformalization
+  - override /cluster@_global_: local
+  - _self_
+
+variant_suffix: "_example"

docs/getting_started.md

@@ -2,6 +2,8 @@
 
 Shinka is a framework that combines Large Language Models (LLMs) with evolutionary algorithms to drive scientific discovery. This guide will help you get started with installing, configuring, and running your first evolutionary experiments.
 
+![](../docs/conceptual.png)
+
 ## Table of Contents
 
 1. [What is Shinka?](#what-is-shinka)
@@ -53,7 +55,7 @@ pip install uv
 
 ```bash
 git clone <shinka-repository-url>
-cd shinka
+cd ShinkaEvolve
 
 # Create virtual environment with Python 3.11
 uv venv --python 3.11
@@ -79,7 +81,7 @@ conda activate shinka
 
 ```bash
 git clone <shinka-repository-url>
-cd shinka
+cd ShinkaEvolve
 pip install -e .
 ```
 
@@ -249,7 +251,7 @@ from shinka.core import run_shinka_eval
 
 def main(program_path: str, results_dir: str):
     """Main evaluation function called by Shinka"""
-    
+
     metrics, correct, error_msg = run_shinka_eval(
         program_path=program_path,
         results_dir=results_dir,
@@ -268,22 +270,22 @@ def main(program_path: str, results_dir: str):
 def validate_packing(run_output):
     """Returns (is_valid: bool, error_msg: str or None)"""
     centers, radii, reported_sum = run_output
-    
+
     # Check constraints (bounds, overlaps, etc.)
     if constraint_violated:
         return False, "Specific error description"
-    
+
     return True, None  # Valid solution
 ```
 
 **2. Metrics Aggregation Function** - Computes fitness and organizes results:
 ```python
 def aggregate_metrics(results, results_dir):
     """Returns metrics dictionary with required structure"""
-    
+
     # Extract data from results
     centers, radii, reported_sum = results[0]
-    
+
     return {
         "combined_score": float(reported_sum),    # PRIMARY FITNESS (higher = better)
         "public": {                               # Visible in WebUI/logs
@@ -331,6 +333,75 @@ The `run_shinka_eval` function returns three values:
 
 ## Advanced Usage
 
+### Resuming Experiments
+
+If you need to pause and resume an evolutionary run, or extend a completed run with more generations, Shinka supports seamless resumption from existing results.
+
+#### How Resuming Works
+
+When you specify an existing `results_dir` that contains a database, Shinka will:
+- Detect the previous run automatically
+- Restore the population database and all program history
+- Resume meta-recommendations from the last checkpoint
+- Continue from the last completed generation
+
+#### Using the CLI (Hydra)
+
+```bash
+# Resume an existing run and extend to 50 generations
+shinka_launch \
+    variant=circle_packing_example \
+    evo_config.results_dir=results_20250101_120000 \
+    evo_config.num_generations=50
+
+# Or with a custom task
+shinka_launch \
+    task=circle_packing \
+    database=island_small \
+    evolution=small_budget \
+    cluster=local \
+    evo_config.results_dir=path/to/previous/results \
+    evo_config.num_generations=100
+```
+
+#### Using the Python API
+
+```python
+from shinka.core import EvolutionRunner, EvolutionConfig
+from shinka.database import DatabaseConfig
+from shinka.launch import LocalJobConfig
+
+# Point to existing results directory
+evo_config = EvolutionConfig(
+    num_generations=50,  # Extend to 50 total generations
+    results_dir="results_20250101_120000",  # Existing results
+    # ... other config parameters ...
+)
+
+job_config = LocalJobConfig(
+    eval_program_path="examples/circle_packing/evaluate.py",
+)
+
+db_config = DatabaseConfig(
+    archive_size=20,
+    num_islands=2,
+)
+
+# Run will automatically detect and resume
+runner = EvolutionRunner(
+    evo_config=evo_config,
+    job_config=job_config,
+    db_config=db_config,
+)
+runner.run()
+```
+
+**Important Notes:**
+- The `num_generations` parameter should be set to the **total** number of generations you want (not additional generations)
+- For example, if you completed 20 generations and want 30 more, set `num_generations=50`
+- The database configuration (number of islands, archive size, etc.) should match the original run
+- All previous progress, including the best solutions and meta-recommendations, will be preserved
+
 ### Environment Management for Local Jobs
 
 When running jobs locally, you have several options for managing Python environments: