Show HN: Link proof assistant Lean to Claude, fix your code's hidden assumptions
1–2 of 2 posts
Re: Show HN: Link proof assistant Lean to Claude, fix your code's hidden assumptions
#2If you haven't heard of Lean, it's a mathematical proof assistant. lean-refine plugs it into Claude Code to find every assumption your code makes but doesn't enforce - then fixes them one by one
Before: https://github.com/savarin/ledger/blob/67d6e236296e4787e8924...
After: https://github.com/savarin/ledger/blob/506584542d1c1c2751e2d...