tripp-smith/lean-lfse

Lean-lfse is the Lazy Financial Scenario Engine, a library and command line tool written in Lean 4, a functional programming language with built in support for formal verification, for describing and evaluating financial scenarios in a way that is auditable and reproducible. The core idea is that financial calculations, such as pricing options, running stress tests, modeling interest rate swaps, and allocating cash through structured tranches, are represented as a graph of lazy computations rather than a flat sequence of function calls. Lazy means a calculation is only actually performed when its result is needed, and once computed, the result is cached and reused everywhere it is referenced. This avoids doing the same expensive calculation twice when many reports share inputs, and it makes it possible to trace exactly which parts of a scenario were evaluated and why. The engine includes a domain specific language, or DSL, for writing financial scenarios directly in Lean code, covering instruments like call and put options, forwards, and swaps. Scenarios can be evaluated from the command line with output in JSON or YAML format, traced to show which nodes were forced, or exported as DOT graph files for visual inspection. A synthetic scenario suite is included to demonstrate realistic workflows: multi asset portfolios evaluated across macro stress regimes, Monte Carlo risk reports with a fixed seed for reproducibility, and asset backed security waterfall allocations. The project also notes several correctness fixes it has hardened against, such as making sure Monte Carlo returns explicit errors instead of silently returning zero for unsupported cases. The README does not state a license for this project.