You wouldn’t be proving the tax code, you’re proving that a procedure follows the tax code. This way you’d be able to know for certain if an AI that tried reducing your taxes actually gives you a valid procedure/result, assuming you can trust the Lean formalization (hint: you can’t given the nature of law, especially if it’s vibe coded like this)