[dev_dan_2]

Great tutorial, really enjoyed it! Personally, I think languages that can check very much at compile time in combinations with LLMs have a bright future ahead. Additionally, if one wanted to give Haskell a try, Lean4 might be a good language to check out before, as it is more modern and ticks many of the same boxes (Still has some unique features, and the communities quite a lot).

Small feedback: - Great flow, explaination, motivation and so on! :) - Typo: "conext" at the bottom - If you want to keyword-hack a bit, you could introduce a paragraph or too about the role the relationship of Lean4 with LLMs/AI ;)

[DennisP]

Vitalik recently wrote about vibe-coding in Lean and assembly language, using proof verification in Lean, saying "if done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before."

https://vitalik.eth.limo/general/2026/05/18/fv.html

[badcryptobitch]

Yeah, his post resulted in a rise in everyone and their mother becoming formal verification "experts" now. But I think he's right. We no longer have good excuses for not trying to secure code with FV in this brave new world of agentic coding

[henryrobbins00]

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