A Quadratic Form Generalization of Rational dinv

These files accompany the paper [TODO].

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.

Input files

• quadratic-form-dinv.pdf (not provided here): a first draft of the paper
• task.md: description of the task to be completed (deferring to quadratic-form-dinv.pdf)
• .environment: specifies the Lean version

Output files (Run with Lean 4.28.0)

• QuadraticDinv/problem.lean: translation of the problem statement into formal language (Lean)
• QuadraticDinv/solution.lean: solution in formal language (Lean)

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

• David Ang
• Kenny Lau
• Seewoo Lee
• Ken Ono