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 statement
• task.md: description of the task to be completed (deferring to Fel_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.

Repository maintainers

• Evan Chen
• Kenny Lau
• Ken Ono
• Jujian Zhang