LEANSTRAL

Summary from the TLDR AI newsletter

Leanstral is an open-source coding agent designed for Lean 4, a proof assistant capable of expressing complex mathematical objects. It is designed to be highly efficient and is trained for operating in realistic formal repositories. Leanstral's weights were released under an Apache 2.0 license. It can be accessed in an agent mode within Mistral vibe and also through a free API endpoint.