Fel's conjecture on syzygies of numerical semigroups
These files accompany the paper arXiv:2602.03716.
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
Fel_Conjecture.tex: natural language problem statementtask.md: description of the task to be completed (deferring toFel_Conjecture.tex).environment: specifies the Lean version
Output files (Run with Lean 4.34.0-rc2)
FelConjecture/problem.lean: translation of the problem statement into formal language (Lean)FelConjecture/solution.lean: solution in formal language (Lean)
Miscellaneous files (not used or written by AxiomProver)
examples.sage: used to verify the worked examples in the paper's exposition
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.