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 en

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/67d6e236296e4787e8924eed860910475d37c138/src/ledger.py https://github.com/savarin/ledger/blob/67d6e236296e4787e8924... After: https://github.com/savarin/ledger/blob/506584542d1c1c2751e2d5819a5e7e29524de924/src/ledger.py https://github.com/savarin/ledger/blob/506584542d1c1c2751e2d...