PoudlardoMar 16

Leanstral: Open-source agent for trustworthy coding and formal proof engineering

Lean 4 paper (2021): https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37

https://mistral.ai/news/leanstral

Show threadjasonjmcgheeMar 16

Curious if anyone else had the same reaction as me

This model is specifically trained on this task and significantly[1] underperforms opus.

Opus costs about 6x more.

Which seems... totally worth it based on the task at hand.

[1]: based on the total spread of tested models

Show threadspeedgooseMar 17
But you can run this model for free on a common battery powered laptop sitting on your laps without cooking your legs.
Show threadhobofanMar 17
Sorry, but what are you talking about? This is a 120B-A6B model, which isn't runnable on any laptop except the most beefed up Macbooks, and then will certainly drain its battery and cook your legs.
Show threadspeedgoose

Yeah my bad, it requires an expensive MacBook.

I think it would still be fine for the legs and on battery for relatively short loads: https://www.notebookcheck.net/Apple-MacBook-Pro-M5-2025-revi...

But 40 degrees and 30W of heat is a bit more than comfortable if you run the agent continuously.

Apple MacBook Pro M5 (2025) review - The fastest single-core performance in the world

Notebookcheck has tested the Apple MacBook Pro 14 M5 with the new M5 SoC, 32 GB RAM and a nano-texture glass mini-LED display.

Notebookcheck
Mar 17 at 7:35amWeb