Leanstral
By Aditi Kabra, Albert Q. Jiang, Andrew Zhao, Dhia Garbaya, Indraneel Mukherjee, Jason Rute, Mert Unsal, Roman Soletskyi, Simon Sorg
Leanstral is a generalist code agent designed for formal theorem proving in Lean 4. Operating within an interactive interface, it saturates miniF2F, solves complex PutnamBench problems, and uncovers unknown code bugs.