Add Lean 4 support

[Racemuis]

Summary

This pull request extends the ShinkaEvolve framework with the automatic formalization and validation in Lean. The implementation is based on the LeanInteract Python package, which interacts with Lean 4 through the Lean REPL.

The generated formalizations are validated by checking the resulting Lean proofs on correctness and completeness.

Motivation

Being a functional programming language and (interactive) theorem prover, Lean allows to express scientific ideas a explicit and verifiable way without requiring the use of higher-level programming languages like Python.

Key Changes

Lean 4 edit support

• Add Lean block markers to /shinka/edit/apply_diff.py.
• Add Lean block markers to /shinka/edit/apply_full.py.
• Add Lean block markers to /shinka/edit/async_apply.py.

Core

• Add Lean support in /shinka/core/runner.py.
• Add /examples/autoformalization/initial.lean - an example of an initial Lean program.
• Add lean-interact to the project's dependencies in pyproject.toml.

Theorem proving and validation

• Add /utils/utils_lean.py - containing all utilities for proof generation and validation through the Lean REPL.
• Add --prover_model flag to eval_hydra.py.
• Propagate the prover_model flag in /shinka/launch/scheduler.py.
• Add /examples/autoformalization/evaluate.py - a simple example of evaluating a Lean program.
• Add .lean option and automated proof generation to /shinka/core/wrap_eval.py.

Usage examples

Installation & Quick start

The evolution of Lean programs follows the principles of the existing ShinkaEvolve framework. However, a Lean 4 installation is required to automatically validate the generated programs.

Tip

You can install Lean using the install-lean command from LeanInteract after cloning the ShinkaEvolve repository and installing all dependencies.

# Clone the repository
git clone https://github.com/SakanaAI/ShinkaEvolve
# Install uv if you haven't already
curl -LsSf https://astral.sh/uv/install.sh | sh  

# If your system doesn't have curl, you can use wget or pip to install it
# wget -qO- https://astral.sh/uv/install.sh | sh
# pip install uv

# Create environment and install Shinka
cd ShinkaEvolve
uv venv --python 3.11
source .venv/bin/activate  # On Windows: .venv\Scripts\activate
uv pip install -e .

# Install Lean 4 via LeanInteract
install-lean  # Requires an elan version >= 4.0.0 (elan --version) 

# Run your first evolution experiment
shinka_launch variant=autoformalization_example

Configuration

The changes made include an LLM-based prover_model for the automated completion of Lean proofs from the generated formalizations. This model is specified in /configs/evolution/*.yaml. Even though the default model is set to gpt-5-nano, it is recommended to use a dedicated prover model like deepseek-ai/DeepSeek-Prover-V2-7B.

/configs/evolution/*_budget.yaml:

...
prover_model: "your_prover_model_here"
...

All other configurations options remain the same.

Note

Some prover models require local hosting. Check out the official guide for setting up local LLM support on directions how to implement this.

Testing

• Evolution and evaluation completed without errors using
  • the OpenAI API (this PR supports the same collection of remote models as the existing framework).
  • locally hosted Qwen models (local hosting on itself is not included in this PR).
  • locally hosted Deepseek models (local hosting on itself is not included in this PR).

Scope

This PR includes changes to support the evolution of programs in Lean 4. It does not feature any changes that support other things, such as hosting local models.

[RobertTLange]

Hi @Racemuis,

Thank you so much for this! Really really exciting. I am personally not a fan of 'stuffing' too much programming language-specific support into the core ShinkaEvolve codebase. But rather have this handled by the user itself (or within an example sub-directory). What I mean by that is not the necessary markers/general syntax utilities but more the evaluation framework itself, e.g., the prover_model and utils_lean.py. I would rather have the following:

main.lean --> evaluate.py --> eval with utils_lean [external to shinka] --> return metrics.json and correct.json

So the entry point would always be the python evaluate.py script, but the evaluation logic (validate_lean) is handled outside of the core codebase. Thereby, Shinka really just focuses on the program optimization/evolution logic. Do you think that would be possible? Also, are there any things that learninteract does not support/limit or is it really just a simple wrapper?

Cheers,
Rob

[Racemuis]

Hi @RobertTLange,

Thank you for your kind reply and helpful comments! I refactored the PR by moving the supporting files to the examples/autoformalization folder, creating a standalone use-case for evolving formalizations in Lean 4.

I aimed to make reduce all changes made in ShinkaEvolve's core: I removed the dependency on the prover_model so that the only changes to the core now include the inclusion of language specific comment markers for the evolving blocks.

All changes made are tested using the OpenAI API, and the evolution and evaluation completed without errors.

Let me know whether there are any other changes I can make! I am happy to incorporate anything.

[RobertTLange]

Superseded by #90, which carries the refreshed SakanaAI:lean_support branch on top of current main. PR #63 still points at Racemuis:lean_support, so it cannot be repointed to the SakanaAI branch.