31–40 of 55 posts
a) Thanks for putting this together! b) Please don't hijack my scrolling. c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
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, explai…
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
a) Thanks for putting this together! b) Please don't hijack my scrolling. c) I really wish Lean were more mature as an application programming language. Its standard library is really lacking.
Please please please don't hijack scrolling :(
I'd inform the webmaster but the telephone number listed on the site is "(123) 456 789", so I guess AI slop is AI slop.
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, explai…
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.
I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…
The number of mentions of Lean in HN submissions aside, how do we gauge that? HN has odd trends like that - a decade ago, we loved everything "Bayesian" - but they don't necessarily translate to anything that's happening in the mainstream.
I built an automated math research system using Lean to verify the results: https://alethean.org