Lean proof to search for US tax loopholes
chaosmanage
14 points
4 comments
November 10, 2026
Related Discussions
Found 5 related stories in 139.8ms across 12,324 title embeddings via pgvector HNSW
- Trove of Never-Before-Seen Records Reveal How the Wealthiest Avoid Income Tax paimapi · 21 pts · September 16, 2026 · 54% similar
- Git for the US Code alansaber · 157 pts · October 28, 2026 · 52% similar
- Dayjob: Tax – evaluating AI agents on 50 professional tax assignments landonxi · 221 pts · October 28, 2026 · 47% similar
- Stealing Reasoning Traces from Proprietary LLM APIs quantumgarbage · 574 pts · August 11, 2026 · 46% similar
- Can Chinese AI (Kimi K3) file American tax returns (TaxCalcBench)? michaelrbock · 12 pts · July 22, 2026 · 46% similar
Discussion Highlights (2 comments)
nylonstrung
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
fwlr
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.