Leanstral 1.5

Leanstral 1.5 is an updated Lean 4 formal proof engineering model with 119B total parameters (6.5B active) designed for automated theorem proving and autoformalization. The model offers a 256k context window, 128k maximum output, and is available for free with support for chat completions, function calling, agents, and structured outputs.