This repository contains artifacts generated by AxiomProver related to the paper arXiv:2605.21718.
For conjecture i where i ∈ {2,5,7,8,9,10}, the input files are:
- the statement of the conjecture in
Conjecture{i}_Statement.tex task.mdthat reads
Please read `Conj{i}_Statement.tex` and formalize Conjecture~\ref{conj:conj{i}}.
.environmentthat readslean-4.28.0(omitted from the current repo)
This repository uses the MIT License. See LICENSE for details.
The formal proofs provided in this work were developed and verified using Lean 4.28.0. Compatibility with earlier or later versions is not guaranteed due to the evolving nature of the Lean 4 compiler and its core libraries.