I'm glad more people are seeing just how applicable lean is to use cases beyond conventional theorem proving and math
I've been working on a project that involves generating monomorphized Rust based on lean specifications and the grind tactic works surprisingly well as an optimizer for stuff like pushdown
Searching a simple model of the Roth IRA for the known backdoors is a good tutorial example. Surprisingly the article just ends there instead of repeating the analysis on the rest of US tax law to find any novel loopholes.