Lokale LLMs · Foto: derekGavey, CC BY 2.0
Leanstral 1.5
Typ
Modell
Lizenz
Apache-2.0
Quelle
Anwendungsfeld
Lokale LLM-Modelle
Mathematik, Forschung und alle, die Software formal beweisen wollen.
Voraussetzungen
Keine besonderen — direkt loslegen.
Spezialmodell für mathematische Beweise und Code-Verifikation in der Beweissprache Lean 4 — 119 Mrd. Parameter, 6,5 Mrd. aktiv, Apache-2.0 (Juli 2026).
Für wen: Mathematik, Forschung und alle, die Software formal beweisen wollen.
Installation
Selbst betreiben: laut Model Card mit vLLM (Tensor-Parallel 4). Ausprobieren ohne Hardware über die Mistral-API.
Erste Schritte
Leanstral schreibt Lean-4-Beweise, die ein Computer prüft — eine Antwort ist also nicht nur plausibel, sondern nachweislich korrekt oder eben nicht. Kontext bis 256.000 Tokens, empfohlen sind bis zu 200.000.
Plattformen: Linux-Server mit GPUs (vLLM) · API
Lizenz & Quelle
- Lizenz: Apache-2.0
- Quelle: HF
- Quelle: Ankündigung
Erfahrungen & Kommentare.
Funktioniert der Modell bei Ihnen? Tipps, Stolperfallen, Varianten — teilen Sie es mit der Community.
Lade Kommentare …
Passt dazu.
Llama 3.1
Der Meta-Klassiker mit 128K Kontext. 8B ist ein sehr solider Allrounder für schwächere Hardware, spricht ordentlich Deutsch.
Llama 3.3
Leistet laut Meta ungefähr so viel wie das riesige 405B-Modell — der Preis-Leistungs-Tipp, wenn man 64 GB (z. B. Mac Studio) hat.
Llama 4 (Scout / Maverick)
Metas MoE-Generation mit sehr großem Kontext und Bildverständnis. Für Heim-Hardware meist zu groß — eher für Server/Mac Studio 128 GB+.