Updates to the README

.gitignore

@@ -6,6 +6,7 @@
 utils/HoleComputation.js
 *.drat
 *.lrat
+cube_checking/cube_gen
 
 ## Nix flake uses .venv directory to set up python stuff
 .venv

README.md

@@ -1,12 +1,14 @@
 # EmptyHexagonLean
 A Lean verification of the _Empty Hexagon Number_, obtained by a [recent breakthrough of Heule and Scheucher](https://arxiv.org/abs/2403.00737).
-The main theorem is that every finite set of 30 or more points must contain a convex and empty 6-gon. The proof is based on generating a CNF formula whose unsatisfiability is formally proved to imply the theorem. This repository contains the formalization code, and it allows the generation of the associated CNF.
+The main theorem is that every finite set of 30 or more points must contain a convex, empty 6-gon. The proof is based on generating a CNF formula whose unsatisfiability is formally proved to imply the theorem. This repository contains the formalization code, and it allows the generation of the associated CNF.
 
 
 
 ## Installing Lean
 
-See the [quickstart](https://lean-lang.org/lean4/doc/quickstart.html) guide from the Lean manual,
+The main part of this repository is a mathematical formalization written in the Lean 4 theorem prover.
+To install Lean on your machine,
+see the [quickstart](https://lean-lang.org/lean4/doc/quickstart.html) guide from the Lean manual,
 or [the extended setup instructions](https://lean-lang.org/lean4/doc/setup.html).
 
 
@@ -37,14 +39,14 @@ Overall structure:
 The project includes scripts for generating the CNFs we formalized against. These must be run inside the `Lean` subfolder.
 
 #### Convex 6-gon
-For `n` points:
+For `n` points, in the `Lake/` directory, run:
 ```
 lake exe encode gon 6 <n>
 ```
 With `n = 17` this CNF can be solved in under a minute on most machines.
 
 #### Convex `k`-hole
-For convex `k`-hole in `n` points:
+For convex `k`-hole in `n` points, in the `Lake/` directory, run:
 ```
 lake exe encode hole <k> <n>
 ```
@@ -61,46 +63,61 @@ In order to verify that the resulting formula $F$ is indeed UNSAT, two things ou
  1) **(Tautology proof)** The formula $F$ is UNSAT iff $F \land C_i$ is UNSAT for every $i$.
  2) **(UNSAT proof)** For each cube $C_i$, the formula $F \land C_i$ is UNSAT.
 
+This repository contains scripts that allow you to check these two proofs.
+
 The **tautology proof** is implied by checking that $F \land (\bigwedge_i \neg C_i)$ is UNSAT, as per Section 7.3 of [Heule and Scheucher](https://arxiv.org/abs/2403.00737).
 
-As a first step, we will generate the main CNF by running:
+As a first step, install the required dependencies:
+1) Clone and compile the SAT solver `cadical` from [its GitHub repository](https://github.com/arminbiere/cadical). Add the `cadical` executable to your `PATH`.
+2) Clone and compile the verified proof checker `cake_lpr` from [its GitHub repository](https://github.com/tanyongkiam/cake_lpr). Add the `cake_lpr` executable to your `PATH`.
+3) Install the `eznf` and `lark` python libraries with `pip install eznf` and `pip install lark`.
+
+Next, generate the main CNF by running:
 ```
 cd Lean
 lake exe encode hole 6 30 ../cube_checking/vars.out > ../cube_checking/6-30.cnf
 ```
 
-Then, inside the `cube_checking` folder, the **tautology proof** can be verified by running `sh verify_tautology`, which boils down to:
+The **tautology proof** can be verified by navigating to the `cube_checking/` directory and running 
+```
+./verify_tautology.sh
+```
+which boils down to:
 ```
 gcc 6hole-cube.c -o cube_gen
 ./cube_gen 0 vars.out > cubes.icnf
 python3 cube_join.py -f 6-30.cnf -c cubes.icnf --tautcheck -o taut_if_unsat.cnf
 cadical taut_if_unsat.cnf tautology_proof.lrat --lrat # this should take around 30 seconds
 cake_lpr taut_if_unsat.cnf tautology_proof.lrat
 ```
-Note that this requires:
-1) The `eznf` python library, which can be installed with `pip install eznf`.
-2) the SAT solver [cadical](https://github.com/arminbiere/cadical) to be in the path,
-3) the verified checker [cake_lpr](https://github.com/tanyongkiam/cake_lpr). As an end result, one sees:
+If proof checking succeeds, you should see the following output:
 
 ```
 s VERIFIED UNSAT
 ```
 
-For the **UNSAT proof**, given the total amount of computation required to run all cubes is probably unfeasible for any verifier, we provide a simple way to verify any given cube to be UNSAT. To generate the formula + cube number $i$ (assuming the steps for the **tautology proof** have been followed), run:
+Because verifying the **UNSAT proof** requires many thousands of CPU hours,
+we provide a simple way to verify that any single cube is UNSAT.
+To generate the formula + cube number $i$ (assuming the steps for the **tautology proof** have been followed), run `./solve_cube.sh` script in the `cube_checking/` directory, which essentially runs:
 ```
 ./cube_gen <i> vars.out > .tmp_cube_<i>
 python3 cube_join.py -f 6-30.cnf -c .tmp_cube_<i> -o with_cube_<i>.cnf
 cadical with_cube_<i>.cnf proof_cube_<i>.lrat --lrat # this should take a few seconds
 cake_lpr with_cube_<i>.cnf proof_cube_<i>.lrat
 ```
-To simplify the process, we have added a bash script `solve_cube.sh`, which can be simply run as (for example, for cube number 42):
+For example, to solve cube number 42, run:
 
 ```
-sh solve_cube.sh 42
+./solve_cube.sh 42
 ```
 The cubes are indexed from 1 to 312418.
 
-To generate the formula + the totality of the cubes for incremental solving, run:
+We **DO NOT RECOMMEND** that the casual verifier runs all cubes,
+as doing so would take many thousands of CPU hours.
+Our verification was completed in a semi-efficient manner using parallel computation,
+which required some custom scripting.
+However, the skeptical reviewer with *lots of computation to spare* can replicate our results.
+To generate the formula and all cubes for incremental solving, run:
 ```
 ./cube_gen 0 vars.out > cubes.icnf
 python3 cube_join.py -f 6-30.cnf -c cubes.icnf --inccnf -o full_computation.icnf