Parity of
These files accompany the paper arXiv:2602.03722.
The formal proofs provided in this work were developed and verified using Lean 4.34.0-rc2. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.
Input files
task.md: natural language description of the task to be completed.environment: specifies the Lean version
Output files (Run with Lean 4.34.0-rc2)
ParityDifferential/problem.lean: translation of the problem statement into formal language (Lean)ParityDifferential/solution.lean: solution in formal language (Lean)
Miscellaneous files (not used or written by AxiomProver)
examples.py: used to show example verification of small cases. Only included for expository reasons and not part of the automated workflow.
Verifying with Comparator
This repository can be verified against the formal problem statement with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator. Then, run the following command:
lake env comparator comparator.json
License
This repository uses the MIT License. See LICENSE for details.