Update README.md

README.md

@@ -15,47 +15,46 @@ For more details about the model and its scope, please read the related [blog po
 
 Leanstral incorporates the following architectural choices:
 
-- **MoE**: 128 experts, 4 active per token  
-- **Model Size**: 119B parameters with 6.5B activated per token  
-- **Context Length**: 256k tokens  
-- **Multimodal Input**: Accepts text and image input, producing text output  
+- **MoE**: 128 experts, 4 active per token
+- **Model Size**: 119B parameters with 6.5B activated per token
+- **Context Length**: 256k tokens
+- **Multimodal Input**: Accepts text and image input, producing text output
 
 Leanstral offers these capabilities:
 
-- **Proof Agentic**: Designed specifically for proof engineering scenarios  
-- **Tool Calling Support**: Optimized for Mistral Vibe  
-- **Vision**: Can analyze images and provide insights  
-- **Multilingual**: Supports English, French, Spanish, German, Italian, Portuguese, Dutch, Chinese, Japanese, Korean, and Arabic  
-- **System Prompt Compliance**: Strong adherence to system prompts  
-- **Speed-Optimized**: Best-in-class performance  
-- **Apache 2.0 License**: Open-source license for commercial and non-commercial use  
-- **Large Context Window**: Supports up to 256k tokens  
+- **Proof Agentic**: Designed specifically for proof engineering scenarios
+- **Tool Calling Support**: Optimized for Mistral Vibe
+- **Vision**: Can analyze images and provide insights
+- **Multilingual**: Supports English, French, Spanish, German, Italian, Portuguese, Dutch, Chinese, Japanese, Korean, and Arabic
+- **System Prompt Compliance**: Strong adherence to system prompts
+- **Speed-Optimized**: Best-in-class performance
+- **Apache 2.0 License**: Open-source license for commercial and non-commercial use
+- **Large Context Window**: Supports up to 256k tokens
 
 ## Recommended Settings
 
-- **Temperature**: 1.0  
-- **Reasoning Effort**:  
-  - `'none'` → Do not use reasoning  
-  - `'high'` → Use reasoning (recommended for complex prompts)  
-  - Use `reasoning_effort="high"` for complex tasks  
-- **Context Length**: ≤ 200k tokens recommended  
+- **Temperature**: 1.0
+- **Reasoning Effort**:
+  - `'none'` → Do not use reasoning
+  - `'high'` → Use reasoning (recommended for complex prompts)
+  Use `reasoning_effort="high"` for complex tasks
+- **Context Length**: ≤ 200k tokens recommended
 
 ## Usage
 
-### Scaffolding
+### Mistral-Vibe
 
-We recommend using `Leanstral 119B A6B` with [Mistral Vibe](https://github.com/mistralai/mistral-vibe).
-
-Make sure the latest version of `mistral-vibe` is installed.
+Use `Leanstral 119B A6B` with [Mistral Vibe](https://github.com/mistralai/mistral-vibe). Install the latest version:
 
 ```sh
 uv pip install mistral-vibe --upgrade
 ```
 
-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*:
+**Add as a provider** in `~/.vibe/config.toml`:
 
-```
+**Official API:**
+
+```toml
 [[providers]]
 name = "mistral-testing"
 api_base = "https://api.mistral.ai/v1"
@@ -70,9 +69,9 @@ thinking = "high"
 temperature = 1.0
 ```
 
-or via a *local server* (see [vLLM](#vllm-recommended)):
+**Local server (via vLLM):**
 
-```
+```toml
 [[providers]]
 name = "vllm"
 api_base = "http://<your-host-url>:8000/v1"
@@ -86,12 +85,11 @@ thinking = "high"
 temperature = 1.0
 ```
 
-Additionally, let's make sure we add a system prompt and that `leanstral` can be used as an agent.
+**System prompt & agent**:
 
-Add the system prompt as defined in [LEAN.md](https://huggingface.co/mistralai/Leanstral-2603/blob/main/LEAN.md) to `~/.vibe/prompts/lean.toml`.
-In addition, add the following file `~/.vibe/agents/lean.toml`:
+Add `~/.vibe/prompts/lean.toml` as in [LEAN.md](https://huggingface.co/mistralai/Leanstral-2603/blob/main/LEAN.md) and create `~/.vibe/agents/lean.toml`:
 
-```
+```toml
 name = "lean"
 display_name = "Lean"
 description = "Specialized mode for Lean 4 code analysis, proof assistance, and theorem proving"
@@ -100,7 +98,7 @@ agent_type = "agent"
 system_prompt_id = "lean"
 ```
 
-A good repository to try out Leanstral could, *e.g.* be [PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd).
+Example repository: [PrimeNumberTheoremAnd](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)
 
 ### Local Deployment
 
@@ -110,15 +108,14 @@ The model can also be deployed with the following libraries, we advise everyone
 
 #### vLLM (recommended)
 
-We recommend using this model with the [vLLM library](https://github.com/vllm-project/vllm)
-to implement production-ready inference pipelines.
+We recommend using this model with the [vLLM library](https://github.com/vllm-project/vllm) to implement production-ready inference pipelines.
 
 **_Installation_**
 
 > [!Tip]
 > We recommend installing vLLM from our custom Docker image that has fixes for
 > Tool Calling and Reasoning parsing in vLLM and uses the latest version of Transformers.
-> We're working with the vLLM team to merge these fixes to vLLM's main as soon as possible.
+> We're working with the vLLM team to merge these fixes to main as soon as possible.
 
 **_Custom Docker_**
 
@@ -133,7 +130,9 @@ docker run -it mistralllm/vllm-ms4:latest
 
 If you prefer, you can also manually install `vllm` from this PR: [Add Mistral Guidance](https://github.com/vllm-project/vllm/pull/37081).
 
-**Note**: It is likely that this PR will be split into smaller PRs and merged to `vllm` main in the coming 1-2 weeks (Stand: 16.03.2026).
+**Note**: 
+It is likely that this PR will be split into smaller PRs and merged to `vllm` main in the coming 1-2 weeks (Stand: 16.03.2026).
+Check latest developments directly on the [PR](https://github.com/vllm-project/vllm/pull/37081).
 
 1. Git clone vLLM:
 ```