This is a formal verification of the manuscript "On the Erdős-Tuza-Valtr Conjecture" in Lean 3.
For any
The Erdős-Tuza-Valtr conjecture is a generalization of the Erdős-Szekeres conjecture.
For any
The case
In our manuscript, we show the first new case
The folder src
contains the Lean 3 source files.
The main theorem theorem main
in the file main/main.lean
.
Note that the cups-caps theroem is also shown in the file main/cap_cup.lean
.
For the minimal set of definitions required for stating the main theorem, we refer to the following files.
config/defs.lean
for the combinatorial model of convexity andlib/list/defs.lean
for the definitions related to a list
The rest are only required for the proof of the main theorem.
The directories config
, etv
, and main
loosely corresponds to Section 2, Section 3 & 4, and Section 5 of the manuscript respectively.