Re:Show HN: Link proof assistant Lean to Claude, fix your co...
by kurinikku on Monday March 30, 2026 @10:53AM
(#47575130)
If 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...