Mistral wypuścił Leanstral 1.5 — model AI do dowodzenia matematycznego

Mistral AI opublikował model Leanstral 1.5, specjalizujący się w formalnym dowodzeniu matematycznym z użyciem języka Lean. Model ma generować dużą liczbę dowodów (tzw. „proof abundance") i jest dostępny dla wszystkich. Leanstral 1.5 to kolejny krok Mistrala w kierunku zastosowań AI w matematyce formalnej i weryfikacji programów.