Mastodawn

Show thread

Thomas Kahle 2d ago

How it's going #leanstral #lean #mistral

Look how it is offering to prove Fermat's last theorem!

Thomas Kahle 2d ago

Habe heute entdeckt, dass in der Fakultät ein bisher ungenutzter Server mit 2x NVIDIA V100 32GB stand. Und nach einem Treiberupdate lief darauf auch das #leanstral Modell mit vernünftiger Geschwindigkeit.

Habe jetzt die 4-Bit Quantisierung genommen und dann passt es mehr oder weniger in den VRAM. Die Kiste hat 1TB normalen RAM, also kein Problem hier.

Bin gespannt, was das kann!

https://huggingface.co/jackcloudman/Leanstral-2603-GGUF

#lean #mistral

jackcloudman/Leanstral-2603-GGUF · Hugging Face

We’re on a journey to advance and democratize artificial intelligence through open source and open science.

Nicolas Fränkel 🇪🇺🇺🇦🇬🇪Mar 20

#Leanstral: #OpenSource foundation for trustworthy #vibecoding

https://mistral.ai/news/leanstral

#MistralAI #formalproof

Leanstral: Open-Source foundation for trustworthy vibe-coding | Mistral AI

First open-source code agent for Lean 4.

Rod2ik 🇪🇺 🇨🇵 🇪🇸 🇨🇱 🇺🇦 🇨🇦 🇬🇱☮🕊️Mar 18

Le #français #MistralAI dévoile #Small4, #Leanstral et #Forge : ce qu’il faut retenir des annonces

https://www.blogdumoderateur.com/mistral-ai-devoile-small-4-leanstral-forge/

Mistral AI dévoile Small 4, Leanstral et Forge : ce qu’il faut retenir des annonces

En l'espace de quelques heures, la société française a enchaîné les annonces, dévoilant un nouveau modèle unifié, un agent de vérification de code et une [...]

BDM

Rod2ik 🇪🇺 🇨🇵 🇪🇸 🇨🇱 🇺🇦 🇨🇦 🇬🇱 ☮🕊️Mar 18

Le #français #MistralAI dévoile #Small4, #Leanstral et #Forge : ce qu’il faut retenir des annonces www.blogdumoderateur.com/mistral-ai-d...

Mistral AI dévoile Small 4, Le...

Mistral AI dévoile Small 4, Leanstral et Forge : ce qu’il faut retenir des annonces

En l'espace de quelques heures, la société française a enchaîné les annonces, dévoilant un nouveau modèle unifié, un agent de vérification de code et une [...]

BDM

Andreas Becker Mar 17

Mistral AI präsentiert das Modell Leanstral, das Quellcode durch Lean 4 mathematisch verifiziert.

Das System nutzt eine Sparse-Architektur mit 119 Milliarden Parametern, wovon 6 Milliarden pro Aufgabe aktiv sind. Im FLTEval-Benchmark erreicht es bei vier Durchläufen 29,3 Punkte und steht unter Apache-2.0-Lizenz bereit.

#Leanstral #MistralAI #Lean4 #OpenSource #News
https://www.all-ai.de/news/news26top/mistral-leanstral-neu

Diese neue KI prüft ihren Code mathematisch auf Fehler

Mistral bringt ein Modell auf den Markt, das Software mathematisch auf Richtigkeit prüft. Die Benchmarks überzeugen.

All-AI.de

N-gated Hacker News Mar 16

🚀✨ Breaking news: #Mistral launches #Leanstral, the "trustworthy" #vibecoding foundation that promises to eliminate the pesky human review process for AI-generated code... because who needs quality assurance when you've got "vibes"? 🙄🎉 In a genius move, revolutionize software engineering by releasing code agents that work like magic wands, making formal proofs as easy as waving goodbye to accountability. 🚀😜
https://mistral.ai/news/leanstral #AIcode #SoftwareEngineering #HackerNews #ngated