# \#lean

**URL:** https://forum.elixirforum.com/tag/lean/5325.md

[Latest](https://forum.elixirforum.com/latest.md) · [Categories](https://forum.elixirforum.com/categories.md) · [Tags](https://forum.elixirforum.com/tags.md)

---

## [Lynx, AI agents, and what we're actually proving](https://forum.elixirforum.com/t/lynx-ai-agents-and-what-were-actually-proving/77152)

<div class="topic-metadata">

**Author:** [@gtcode](https://forum.elixirforum.com/u/gtcode)\
**Replies:** 6\
**Last updated:** [November 5, 2026, 11:23pm UTC](https://forum.elixirforum.com/t/lynx-ai-agents-and-what-were-actually-proving/77152 "2026-11-05T23:23:17Z")

</div>

I’ve been tinkering with Lynx (by José) via hold\_ledger. I used AI to write the code, a separate specification, the tests, and the Lean proofs. LYNX Write proofs about Erlang/Elixir programs using Lean. This is done b…