Leanstral is the first open-source code agent designed for Lean 4, a proof assistant capable of expressing complex mathematical objects such as perfectoid spaces and software specifications like properties of Rust fragments.
Built as part of the Mistral Small 4 family, it combines multimodal capabilities and an efficient architecture, making it both performant and cost-effective compared to existing closed-source alternatives.
For more details about the model and its scope, please read the related blog post.
from openai import OpenAI
from huggingface_hub import hf_hub_download
# Modify OpenAI's API key and API base to use vLLM's API server.
openai_api_key = "EMPTY"
openai_api_base = "<your-host-url>"
client = OpenAI(
api_key=openai_api_key,
base_url=openai_api_base,
)
TEMP = 1.0
MAX_TOK = 32000
REASONING = "high" # switch to 'none' for faster answers
models = client.models.list()
model = models.data[0].id
prompt = """Define the transition rules as an inductive proposition.
This choice provides better support for proving properties about valid transitions and is generally more natural for modeling state machines in Lean, where you want to express logical rules rather than just computing a yes/no vale for each possible transition."""
messages = [
{
"role": "user",
"content": [
{
"type": "text",
"text": prompt,
},
],
},
]
response = client.chat.completions.create(
model=model,
messages=messages,
temperature=TEMP,
max_tokens=MAX_TOK,
reasoning_effort=REASONING,
)
print("Content")
print(response.choices[0].message.content)
pritn("Reasoning")
print(response.choices[0].message.reasoning)
Example Content:
Expand</summary To define transaction rules as an inductive proposition in Lean, you can create an inductive type that captures the valid transitions between states. This approach is particularly useful for modeling state machines and proving properties about transitions, such as invariants.
Here is an example of how to define an inductive proposition for valid transitions in a simple counter machine:
-- Example: Counter that can only increment by 1 (no decrement, no shortcuts)
inductive ValidTransition : Nat → Nat → Prop
| step1 : ∀ s, ValidTransition s (s + 1) -- Core transition: s → s+1
| step2 : ∀ s, ValidTransition s (2 * s) -- Bonus: s → 2s (optional)
| zero_step : ValidTransition 0 0 -- Additional special case
lemma reach_any_positive : ∀ n > 0, ValidTransition 0 n := by
induction n with
| zero => contradiction
| succ n ih =>
cases' Nat.eq_zero_or_pos n with h h
· simp [h]
· have : ValidTransition 0 (n + 1) := by
cases' h with _ ih -- Wait, this is messy...
In this example, ValidTransition is defined as an inductive proposition with constructors step1, step2, and zero_step. The step1 constructor allows for any state to transition to the next state by incrementing by 1, while step2 allows for doubling the state. The zero_step constructor is a special case for the initial state 0.
The lemma reach_any_positive aims to prove that any positive natural number is reachable from the initial state 0 through valid transitions. The proof uses induction on n, but due to simplification issues, the current approach may not be the most effective.
A more concise and effective way to define and prove properties about transitions is to use a simpler model, such as the following:
-- Simpler model for counter transitions (suffices for proofs)
inductive CounterTrans : Nat → Nat → Prop
| valid : ∀ n, CounterTrans n (n + 1)
lemma reach_positive : ∀ n > 0, CounterTrans 0 n
-- Proof is now trivial (by induction)
In this simpler model, CounterTrans is defined with a single constructor valid, which allows for any state to transition to the next state by incrementing by 1. The lemma reach_positive is straightforward to prove by induction, leveraging the simplicity of the transition rules.
This approach ensures that the proof remains concise and effective, avoiding unnecessary complexity in the transition rules. By using inductive propositions, we can effectively reason about state transitions and prove properties about the system.
Tool-Calling
You can add tools to the chat completion as follows:
prompt = """I have the following Lean 4 code snippet and want to check if it compiles and runs without errors. Can you run it for me and let me know the result?
tools = [{ "type": "function", "function": { "name": "lean_run_code", "description": "Run or compile an independent Lean code snippet or file and return the result or error message.", "parameters": { "type": "object", "properties": { "code": { "type": "string", "description": "Lean code snippet to run or compile. Either this or file_path must be provided." }, "file_path": { "type": "string", "description": "Path to the Lean file to run or compile. Either this or code must be provided." } }, } } }]
_Example Tool Calls_:
Expand</summary
`Function(arguments='{"code": "inductive State where\\n | idle\\n | busy\\n | error\\n\\ndef transition : State → State → Bool\\n | .idle, .busy => true\\n | .busy, .idle => true\\n | .busy, .error => true\\n | _, _ => false\\n\\n#eval transition .idle .busy"}', name='lean_run_code')`
## License
This model is licensed under the [Apache 2.0 License](https://www.apache.org/licenses/LICENSE-2.0.txt).
*You must not use this model in a manner that infringes, misappropriates, or otherwise violates any third party’s rights, including intellectual property rights.*
Files
14 files · 121 GBWeights 121 GB (safetensors). Sizes and sha256 from the signed manifest.
mistralai <huggingface.co/mistralai>Newsgroups: alt.freeweights.mistralSubject: 
mlx-community