Show HN：美国 IRS 联邦税表的机器可校验形式化概念验证

一个开源概念验证项目把美国 IRS 联邦个人所得税的税表与填报说明编码为带引用的机器可校验数据，并配一个引导式自助报税问答作为首个客户端。项目覆盖 2,384 行计算逻辑，全部使用约二十种封闭原子操作，0 行使用不透明函数；TypeScript 与 Lean 两套独立求值器在 1,648 个用例、2,895,826 个行值上对比 0 差异。软件不申报、不签名、不传输税表，数据不离开本机。