parity-differential

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

parity-differential

★ 27 Open GitHub ↗

Lean formalizations for the paper "Parity of k-differentials in genus zero and one"

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

[![Logo for Axiom Math](https://raw.githubusercontent.com/AxiomMath/parity-differential/main/logo.svg)](https://axiommath.ai/)

# Parity of $k$-differentials in genus zero and one

These files accompany the paper [arXiv:2602.03722](https://arxiv.org/abs/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.

## Input files

- [`task.md`](task.md): natural language description of the task to be completed
- [`.environment`](.environment): specifies the Lean version

## Output files (Run with Lean 4.26.0)

- [`ParityDifferential/problem.lean`](ParityDifferential/problem.lean): translation of the problem statement into formal language (Lean)
- [`ParityDifferential/solution.lean`](ParityDifferential/solution.lean): solution in formal language (Lean)

## Miscellaneous files (not used or written by AxiomProver)

- [`examples.py`](examples.py): used to show example verification of small cases.
  Only included for expository reasons and not part of the automated workflow.

## License

This repository uses the MIT License. See [LICENSE](LICENSE) for details.

## Repository maintainers

- [Evan Chen](https://github.com/vEnhance)
- [Kenny Lau](https://github.com/kckennylau)
- [Ken Ono](https://github.com/kenono691)
- [Jujian Zhang](https://github.com/jjaassoonn)

parity-differential

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README