These files accompany the paper arXiv:2602.03722.
The formal proofs provided in this work were developed and verified using Lean 4.26.0. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.
task.md: natural language description of the task to be completed.environment: specifies the Lean version
ParityDifferential/problem.lean: translation of the problem statement into formal language (Lean)ParityDifferential/solution.lean: solution in formal language (Lean)
examples.py: used to show example verification of small cases. Only included for expository reasons and not part of the automated workflow.
This repository uses the MIT License. See LICENSE for details.