Update README.md

README.md

@@ -4,9 +4,11 @@ library_name: vllm
 ---
 # Leanstral 119B A6B
 
-Leanstral is the firsd open-source code agent designed for Lean4, a proof assistant capable to express complex mathematical objects such as [perfectoid spaces](https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/) and software specifications like [properties of Rust fragments](https://github.com/AeneasVerif/aeneas)
+Leanstral is the first open-source code agent designed for [Lean4](https://github.com/leanprover/lean4), a proof assistant capable to express complex mathematical objects such as [perfectoid spaces](https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/)
+and software specifications like [properties of Rust fragments](https://github.com/AeneasVerif/aeneas)
 
-Built as par of the [Mistral Small 4 family](https://huggingface.co/collections/mistralai/mistral-small-4), it has multimodal capabilities, efficient architecture it is both formant and cost-efficient against existing closed-source competitors.
+Built as par of the [Mistral Small 4 family](https://huggingface.co/collections/mistralai/mistral-small-4), 
+it has multimodal capabilities, efficient architecture it is both formant and cost-efficient against existing closed-source competitors.
 
 For more information about the model and its scope, please read the related [blog post](https://mistral.ai/news/leanstral)
 
@@ -50,8 +52,8 @@ Make sure the latest version of `mistral-vibe` is installed.
 uv pip install mistral-vibe --upgrade
 ```
 
-Once installed, make sure to add the `leanstral` as a provider. You can either add Mistral's API endpoint or your local server as a provider.
-Add leanstral as a provider to your config (`~/.vibe/config.toml`) either via the official API:
+Once installed, let's add the `leanstral` as a provider.
+Add the model as a provider to your config (`~/.vibe/config.toml`) either via *the official API*:
 
 ```
 [[providers]]
@@ -68,10 +70,20 @@ thinking = "high"
 temperature = 1.0
 ```
 
-or via a local server:
+or via a *local server* (see [vLLM](#vllm-recommended)):
 
 ```
-
+[[providers]]
+name = "vllm"
+api_base = "http://<your-host-url>:800/v1"
+reasoning_as_structured_content = true
+reasoning_field_name = "reasoning_content"
+[[models]]
+name = "labs-leanstral-2603"
+provider = "mistral-testing"
+alias = "leanstral"
+thinking = "high"
+temperature = 1.0
 ```
 
 Additionally, let's make sure we add a system prompt and that `leanstral` can be used as an agent.