If you're excited about the relationship of Lean4 to LLMs/AI (like I am), you might find my recent post interesting [1].

TL;DR: I'm using automated theorem provers within my research on AI for automated algorithm design. To make it easier to run/benchmark different models/harnesses, I created an open-source Python package called OpenATP [2]. I recently added support to use Grok 4.5 in the OpenCode harness as a prover and found it to be surprisingly competitive with Claude Code and Codex at a fraction the cost and wall-clock time.

[1] https://news.ycombinator.com/item?id=49010310

[2] https://github.com/henryrobbins/open-atp