TL;DR: I'm working on a Python package called OpenATP [1] that provides a common interface to coding agents for automated theorem proving in Lean. In the latest release, I added support for Leanstral 1. 5 [2,3], Grok, and Kimi Code [4].
Source: [Hacker News](https://news.ycombinator.com/item?id=49010310)