Rendered at 08:58:57 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
nylonstrung 21 hours ago [-]
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
alansaber 20 hours ago [-]
It gets a lot of pushback in the legal domain (naturally), but I feel like the utility is already clearly evident.
20 hours ago [-]
fwlr 21 hours ago [-]
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.
alansaber 20 hours ago [-]
Thanks. Sorry if you feel like it ends abruptly, i've been following up on this today.
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