Create README.md

README.md

@@ -0,0 +1,31 @@
+# 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)
+
+Built as par of the Mistral Small 4 family, 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]()
+
+## Key Features
+
+Leanstral consists of the following architectural choices:
+
+- MoE: 128 experts and 4 active.
+- 119B with 6.5B activated parameters per token.
+- 256k Context Length.
+- Multimodal Input: Accepts both text and image input, with text output.
+
+Leanstral offers the following capabilities:
+
+- **Proof Agentic**: Leanstral is specifically design to perform proof engineer scenarios.
+- **Vision**: Enables the model to analyze images and provide insights based on visual content, in addition to text.
+- **Multilingual**: Supports dozens of languages, including English, French, Spanish, German, Italian, Portuguese, Dutch, Chinese, Japanese, Korean, Arabic.
+- **System Prompt**: Maintains strong adherence and support for system prompts.
+- **Speed-Optimized**: Delivers best-in-class performance and speed.
+- **Apache 2.0 License**: Open-source license allowing usage and modification for both commercial and non-commercial purposes.
+- **Large Context Window**: Supports a 256k context window.
+
+### Examples
+
+## Usage
+